nyuuzyou/wikis huggingface dataset:
Element of *-Algebra is Hermitian iff Hermitian in Unitization

== Theorem ==
Let $\tuple {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $A_+$ be the unitization of $A$.
Define:
:$\tuple {u, \lambda}^\ast = \tuple {u^\ast, \overline \lambda}$
for each $\tuple {u, \lambda} \in A_+$.
Let $a \in A$.
Then $a$ is Hermitian in $A$ $\tuple {a, 0}$ is Hermitian in $A_+$. 
== Proof ==
Suppose that $a$ is Hermitian. 
Then $a = a^\ast$.
Hence $\tuple {a, 0}^\ast = \tuple {a^\ast, 0} = \tuple {a, 0}$.
So $\tuple {a, 0}$ is Hermitian in $A_+$.
Now suppose that $\tuple {a, 0}$ is Hermitian in $A_+$.
Then we have:
:$\tuple {a, 0}^\ast = \tuple {a, 0}$
while:
:$\tuple {a, 0}^\ast = \tuple {a^\ast, 0}$
So we have $\tuple {a, 0} = \tuple {a^\ast, 0}$ and so $a = a^\ast$.
So $a$ is Hermitian in $A$.
Category:*-Algebras
Element of C*-Algebra is Positive iff Positive in Unitization

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra. 
Let $A_+$ be the unitization of $A$.
Define:
:$\tuple {x, \lambda}^\ast = \tuple {x^\ast, \overline \lambda}$
for each $\tuple {x, \lambda} \in A_+$.
Let $\norm {\, \cdot \,}_\ast$ be such that $\struct {A_+, \ast, \norm {\, \cdot \,}_\ast}$ is a unital $\text C^\ast$-algebra.
Let $a \in A$.
Then $a$ is positive in $A$ $\tuple {a, 0}$ is positive in $A_+$. 
=== Corollary ===
== Proof ==
The existence of $\norm {\, \cdot \,}_\ast$ follows from:
:Existence of Unitization of C*-Algebra if $A$ is non-unital
:Existence of Unique C* Norm on Unitization of Unital C*-Algebra if $A$ is unital
From Element of *-Algebra is Hermitian iff Hermitian in Unitization:
:$a$ is Hermitian in $A$ $\tuple {a, 0}$ is Hermitian in $A_+$
From Spectrum of Element in Unitization of Unital Algebra and the definition of the spectrum in a non-unital algebra, we have:
:$\map {\sigma_A} a \subseteq \map {\sigma_{A_+} } {\tuple {a, 0} } \subseteq \map {\sigma_A} a \cup \set 0$
Suppose that $a$ is positive in $A$, then:
:$\map {\sigma_A} a \subseteq \hointr 0 \infty$
and so:
:$\map {\sigma_{A_+} } {\tuple {a, 0} } \subseteq \hointr 0 \infty$
so $\tuple {a, 0}$ is positive in $A_+$.
Suppose that $\tuple {A, 0}$ is positive in $A_+$, then:
:$\map {\sigma_{A_+} } {\tuple {a, 0} } \subseteq \hointr 0 \infty$
and so:
:$\map {\sigma_A} a \subseteq \map {\sigma_{A_+} } {\tuple {a, 0} } \subseteq \hointr 0 \infty$
so $\map {\sigma_A} a$ and $a$ is positive in $A$.
Category:Positive Elements of C*-Algebras
Category:Element of C*-Algebra is Positive iff Positive in Unitization
Element of C*-Algebra is Positive iff Positive in Unitization/Corollary

== Corollary ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra. 
Let $A_+$ be the unitization of $A$.
Define:
:$\tuple {x, \lambda}^\ast = \tuple {x^\ast, \overline \lambda}$
for each $\tuple {x, \lambda} \in A_+$.
Let $\norm {\, \cdot \,}_\ast$ be such that $\struct {A_+, \ast, \norm {\, \cdot \,}_\ast}$ is a unital $\text C^\ast$-algebra.
Let $\le_A$ be the canonical preordering of $A$.
Let $\le_+$ be the canonical preordering of $A_+$.
Let $a, b \in A$.
Then:
:$a \le_A b$ $\tuple {a, 0} \le_+ \tuple {b, 0}$
== Proof ==
We have that $a \le_A b$ :
:$b - a$ is positive in $A$.
From Element of C*-Algebra is Positive iff Positive in Unitization, this is the case :
:$\tuple {b - a, 0}$ is positive in $A_+$.
We have $\tuple {b - a, 0} = \tuple {b, 0} - \tuple {a, 0}$, hence this is equivalent to $\tuple {b, 0} - \tuple {a, 0}$ positive.
This is therefore equivalent to $\tuple {a, 0} \le_+ \tuple {b, 0}$.
Category:Element of C*-Algebra is Positive iff Positive in Unitization
Element of Center in Group whose Order is Power of 2

== Theorem ==
Let $n \in \Z$ be an integer such that $n \ge 2$.
Let $G$ be a group whose order is $2^n$.
Let $x \in G$ be of order $2^{n - 1}$ in $G$.
Then $x^{2^{n - 2} }$ is an element of the center of $G$.
== Proof ==
Let $H = \gen x$ be the subgroup of $G$ generated by $x$.
We have that the index of $H$ in $G$ is $2$.
Then by Subgroup of Index 2 is Normal, $H$ is normal in $G$.
Let $y = x^{2^{n - 2} }$.
We have that $y \in H$, by definition of the construction of $H$.
Then the order of $y$ in $G$ is $2$.
As $H$ is normal, we have:
:$\forall g \in G: g y g^{-1} \in H$
By Order of Conjugate Element equals Order of Element, $g y g^{-1}$ is also of order $2$.
We can write $g y g^{-1} = x^m$ for some $m \in \Z$.
By Order of Power of Group Element, we have:
:$2 = \dfrac {2^{n - 1} } {\gcd \set {m, 2^{n - 1} } }$
This leads to:
:$\gcd \set {m, 2^{n - 1} } = 2^{n - 2}$
We have $0 < m < 2^{n - 1}$ and $2^{n - 2} \divides m$.
This forces $m = 2^{n - 2}$ and $g y g^{-1} = y$.
It follows that $g y = y g$.
Hence $y = x^{2^{n - 2} }$ is an element of the center of $G$.
== Sources ==
* : Chapter $8$: Homomorphisms, Normal Subgroups and Quotient Groups: Exercise $11$
Category:Centers of Groups
Element of Class is Subset of Union of Class

== Theorem ==
Let $A$ be a class.
Let $\ds \bigcup A$ denote the union of $A$.
Let $x \in A$.
Then:
:$x \subseteq \ds \bigcup A$
== Proof ==
Let $x \in A$.
By definition of class, $x$ is a set.
Let $y \in x$.
By definition of union of $A$:
:$\ds \bigcup A := \set {y: \exists x \in A: y \in x}$
It follows directly from that definition that:
:$y \in \ds \bigcup A$
The result follows by definition of subset.
Category:Class Union
Element of Completely Prime Filter iff Does not Precede Supremum of Relative Complement

== Theorem ==
Let $\struct{L, \preceq}$ be a complete lattice.
Let $p$ be a completely prime filter $p$ of $L$.
Let $a \in L$.
Then:
:$a \in p$
:
:$a \npreceq \bigvee \paren{L \setminus p}$
where:
:$L \setminus p$ denotes the relative complement of $p$ in $L$
:$\bigvee \paren{L \setminus p}$ denotes the supremum of $L \setminus p$
== Proof ==
=== Necessary Condition ===
We show the contrapositive statement:
:$a \preceq \bigvee \paren{L \setminus p} \implies a \notin p$
Let:
:$a \preceq \bigvee \paren{L \setminus p}$
By definition of completely prime filter:
:$\bigvee \paren{L \setminus p} \in L \setminus p$ 
By definition of relative complement:
:$\bigvee \paren{L \setminus p} \notin p$ 
By definition of filter:
:$a \notin p$
=== Sufficient Condition ===
Let:
:$a \npreceq \bigvee \paren{L \setminus p}$
By definition of supremum:
:$a \notin L \setminus p$
By definition of relative complement:
:$a \in p$
Category:Completely Prime Filters
Element of Cyclic Group is not necessarily Generator

== Theorem ==
Let $\gen g = G$ be a cyclic group.
Let $a \in G$
Then it is not necessarily the case that $a$ is also a generator of $G$.
== Proof ==
Consider the multiplicative group of real numbers $\struct {\R_{\ne 0}, \times}$.
Consider the subgroup $\gen 2$ of $\struct {\R_{\ne 0}, \times}$ generated by $2$.
By definition, $\gen 2$ is a cyclic group.
Consider the element $4 \in \struct {\R_{\ne 0}, \times}$.
We have that $4 = 2^2$.
Thus $4 \in \gen 2$.
There exists no $n \in \Z$ such that $4^n = 2$.
But $2 \in \gen 2$.
Thus $\gen 2$ is not generated by $4$.
That is, $4$ is not a generator of $\gen 2$.
Hence the result, by Proof by Counterexample.
== Sources ==
* : $\S 39$. Cyclic Groups
Category:Cyclic Groups
Element of Every Transitive-Closed Class is Ordinal

== Theorem ==
Let $x$ be a set such that $x$ is an element of every transitive-closed class.
Then $x$ is an ordinal.
== Proof ==
== Sources ==
* : Chapter $5$: Ordinal Numbers: $\S 2$ Ordinals and transitivity: Exercise $2.1$
Category:Transitive-Closed Classes
Category:Ordinals
Element of Finite Group is of Finite Order

== Theorem ==
In any finite group, each element has finite order.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : Chapter $5$: Subgroups: Exercise $15$
* : Chapter $3$: Elementary consequences of the definitions: Definition $3.9$: Remark $1$
Category:Finite Groups
Category:Order of Group Elements
Category:Element of Finite Group is of Finite Order
Element of Finite Group is of Finite Order/Proof 1

== Theorem ==
== Proof ==
Let $G$ be a group whose identity is $e$.
From Element has Idempotent Power in Finite Semigroup, for every element in a finite semigroup, there is a power of that element which is idempotent.
As $G$, being a group, is also a semigroup, the same applies to $G$.
That is:
:$\forall x \in G: \exists n \in \N_{>0}: x^n \circ x^n = x^n$
From Identity is only Idempotent Element in Group, it follows that:
:$x^n \circ x^n = x^n \implies x^n = e$
So $x$ has finite order.
== Sources ==
* : Chapter $\text {I}$: The Group Concept: $\S 8$: The Order (Period) of an Element
Category:Element of Finite Group is of Finite Order
Element of Finite Ordinal iff Subset

== Theorem ==
Let $m, n$ be distinct finite ordinals.
Then:
:$m \in n \iff m \subseteq n$
== Proof ==
Let $m \in n$.
Since $n$ is an ordinal, it is transitive.
Therefore, it follows directly that $m \subseteq n$.
Now let $m \subseteq n$.
We have by hypothesis that $m \ne n$.
From Natural Numbers are Comparable it follows that either $m \in n$ or $n \in m$.
Suppose $n \in m$.
Then $\exists x \in m: m \subseteq x$ which contradicts Finite Ordinal is not Subset of one of its Elements.
The only option left is that $m \in n$.
Hence the result.
== Sources ==
* : $\S 13$: Arithmetic
Category:Finite Ordinals
Category:Subsets
Element of Free Group can be Expressed Uniquely as Finite Product

== Theorem ==
Let $G$ be a free group.
Let $x \in G$ be an element of $G$ other than the identity element.
Then $x$ can be expressed uniquely in the form: 
:$a^\alpha b^\beta \dotsm r^\sigma$
where:
:adjacent elements $a, b, \ldots, r$ of $a^\alpha b^\beta \dotsm r^\sigma$ are distinct elements of $G$
:$\alpha, \beta, \ldots, \sigma$ are non-zero integers.
== Proof ==
== Sources ==
* 
* 
Category:Free Groups
Element of Group Not Conjugate to Proper Subgroup

== Theorem ==
Let $G$ be a finite group.
Let $H$ be a proper subgroup of $G$.
Then there is at least one element of $G$ not contained in $H$ or in any of its conjugates.
== Proof ==
Let $S \subseteq G$ be defined by:
:$S := \set {g \in G: \exists h \in H, a \in G: g = a h a^{-1} }$
It is required to show that $S \ne G$.
Let $\map {N_G} H$ be the normalizer of $H$ in $G$.
By Subgroup is Subgroup of Normalizer, $H \le \map {N_G} H$.
Therefore, by definition of index:
:$\index G {\map {N_G} H} \le \index G H$
Each of the conjugates of $H$ has $\order H$ elements.
By Number of Distinct Conjugate Subsets is Index of Normalizer, there are $\index G {\map {N_G} H}$ conjugates.
Therefore:
:$\card S \le \order H \index G {\map {N_G} H}$
with equality all conjugates of $H$ are disjoint.
Combining this with the earlier inequality, we find that:
:$\card S \le \order H \index G H = \order G$
Now if $H$ is normal in $G$, then by Normalizer of Subgroup is Largest Subgroup containing that Subgroup as Normal Subgroup:
:$\index G {\map {N_G} H} < \index G H$
for $\map {N_G} H = G$ in that case, and $H$ is a proper subgroup.
If $H$ is not normal in $G$, then it has multiple conjugates.
By Conjugate of Subgroup is Subgroup, they all are subgroups of $G$.
In particular, then, the identity of $G$ is common to all of them.
Hence they are not disjoint, and:
:$\card S < \order H \index G {\map {N_G} H}$
In either case, it follows that:
:$\card S < \order G$
as desired.
== Sources ==
* : Chapter $2$: Conjugacy, Normal Subgroups, and Quotient Groups: $\S 49 \beta$
Category:Conjugacy
Element of Group is in Unique Coset of Subgroup/Left

== Theorem ==
Let $G$ be a group.
Let $H$ be a subgroup of $G$.
Let $x \in G$.
There exists a exactly one left coset of $H$ containing $x$, that is: $x H$
== Proof ==
Follows directly from:
* Left Congruence Modulo Subgroup is Equivalence Relation
* Element in its own Equivalence Class.
== Also see ==
* Element of Group is in Unique Right Coset of Subgroup
== Sources ==
* : $\S 42.5$ Another approach to cosets
Category:Element of Group is in Unique Coset of Subgroup
Element of Group is in Unique Coset of Subgroup/Right

== Theorem ==
Let $G$ be a group.
Let $H$ be a subgroup of $G$.
Let $x \in G$.
There exists a exactly one right coset of $H$ containing $x$, that is: $H x$
== Proof ==
Follows directly from:
* Right Congruence Modulo Subgroup is Equivalence Relation
* Element in its own Equivalence Class.
== Also see ==
* Element of Group is in Unique Left Coset of Subgroup
== Sources ==
* : $\S 42.5$ Another approach to cosets
Category:Element of Group is in Unique Coset of Subgroup
Element of Group is in its own Coset/Left

== Theorem ==
Let $G$ be a group.
Let $H$ be a subgroup of $G$.
Let $x \in G$.
Let:
: $x H$ be the left coset of $x$ modulo $H$.
Then:
: $x \in x H$
== Proof ==
Let $e$ be the identity of $G$.
Then:
== Also see ==
* Element of Group is in its own Right Coset
== Sources ==
* : $\S 42.5$ Another approach to cosets
* : Chapter $5$: Cosets and Lagrange's Theorem: Definition $5.1$: Remark $2$
Category:Element of Group is in its own Coset
Element of Group is in its own Coset/Right

== Theorem ==
Let $G$ be a group.
Let $H$ be a subgroup of $G$.
Let $x \in G$.
Let:
: $H x$ be the right coset of $x$ modulo $H$.
Then:
: $x \in H x$
== Proof ==
Let $e$ be the identity of $G$.
Then:
== Also see ==
* Element of Group is in its own Left Coset
== Sources ==
* : $\S 42.5$ Another approach to cosets
Category:Element of Group is in its own Coset
Element of Horizontal Space as Horizontal Lift of Vector Field

== Theorem ==
Let $\tilde M, M$ be smooth manifolds.
Let $\pi : \tilde M \to M$ be a smooth submersion.
Let $\tilde g$ be a Riemannian metric on $\tilde M$.
Let $H_x$ be a horizontal tangent space of $\tilde M$ at $x$.
Let $\map {\mathfrak{X}} M$ be the space of smooth vector fields of $M$.
Then for every $x \in \tilde M$ and every $v \in H_x$ there is a vector field $X \in \map {\mathfrak{X}} M$ whose horizontal lift $\tilde X$ satisfies $\tilde X_x = v$.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Methods for Constructing Riemannian Metrics
Category:Riemannian Geometry
Element of Integral Domain Divides Zero

== Theorem ==
Let $\struct {D, +, \circ}$ be an integral domain whose zero is $0_D$.
Then every element of $D$ divides $0_D$:
:$\forall x \in D: x \divides 0_D$
== Proof ==
By definition, an integral domain is a ring.
So, from Ring Product with Zero:
:$\forall x \in D: 0_D = x \circ 0_D$
The result follows from the definition of divisor.
== Sources ==
* : $\S 62.1$ Factorization in an integral domain: $\text{(i)}$
Category:Integral Domains
Element of Integral Domain is Divisor of Itself

== Theorem ==
Let $\struct {D, +, \circ}$ be an integral domain whose unity is $1_D$.
Then every element of $D$ is a divisor of itself:
:$\forall x \in D: x \divides x$
== Proof ==
Follows directly from the definition of divisor:
:$\forall x \in D: \exists 1_D \in D: x = 1_D \circ x$
Category:Integral Domains
Element of Integration/Examples/Element of Area

== Example of Element of Integration ==
Consider the definite integral:
:$\ds \int_a^b \map f x \rd x$
This gives the area under the curve whose locus is given by $y = \map f x$
Hence the element of integration $\map f x \rd x$ can be interpreted as an infinitesimal strip of area.
These are then summed to find the total area under the curve.
== Sources ==
* 
* 
Category:Examples of Elements of Integration
Element of Leibniz Harmonic Triangle as Sum of Elements on Diagonal from Below

== Theorem ==
Consider the Leibniz harmonic triangle:
Let $\tuple {n, m}$ be the element in the $n$th row and $m$th column.
Then:
:$\tuple {n, m} = \ds \sum_{k \mathop \ge 0} \tuple {n + 1 + k, m + k}$
=== Lemma 1 ===
=== Lemma 2 ===
== Proof ==
Taking $r \to \infty$ in Lemma 2:
== Sources ==
* : $35$
* : $35$
Category:Leibniz Harmonic Triangle
Category:Element of Leibniz Harmonic Triangle as Sum of Elements on Diagonal from Below
Element of Leibniz Harmonic Triangle as Sum of Elements on Diagonal from Below/Lemma 1

== Theorem ==
Consider the Leibniz harmonic triangle:
Let $\tuple {n, m}$ be the element in the $n$th row and $m$th column.
Then:
:$\tuple {n, m} = \tuple {n + 1, m} + \tuple {n + 1, m + 1}$
That is, each number in the Leibniz harmonic triangle is equal to the sum of the number below it and the number to the right of that number.
This is similar to Pascal's Rule for Pascal's triangle.
== Proof ==
Category:Leibniz Harmonic Triangle
Category:Element of Leibniz Harmonic Triangle as Sum of Elements on Diagonal from Below
Element of Leibniz Harmonic Triangle as Sum of Elements on Diagonal from Below/Lemma 2

== Theorem ==
Consider the Leibniz harmonic triangle:
Let $\tuple {n, m}$ be the element in the $n$th row and $m$th column.
Then:
:$\ds \forall r \in \N_{>0}: \tuple {n, m} = \tuple {n + r, m + r} + \sum_{k \mathop = 1}^r \tuple {n + k, m + k - 1}$
That is, each number in the Leibniz harmonic triangle is equal to the sum of the number below it, $\paren {r - 1}$ numbers diagonally below that number, and the number to the right of the last number.
This is similar to Rising Sum of Binomial Coefficients (Hockey-stick Identity) for Pascal's triangle.
== Proof ==
Proof by induction:
For all $r \in \N_{>0}$, let $\map P r$ be the proposition:
:$\ds \tuple {n, m} = \tuple {n + r, m + r} + \sum_{k \mathop = 1}^r \tuple {n + k, m + k - 1}$
=== Basis for the Induction ===
$\map P 1$ is:
:$\tuple {n, m} = \tuple {n + 1, m + 1} + \tuple {n + 1, m}$
which is shown in Lemma 1.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P s$ is true, where $s \ge 1$, then it logically follows that $\map P {s + 1}$ is true.
So this is our induction hypothesis:
:$\ds \tuple {n, m} = \tuple {n + s, m + s} + \sum_{k \mathop = 1}^s \tuple {n + k, m + k - 1}$
Then we need to show:
:$\ds \tuple {n, m} = \tuple {n + s + 1, m + s + 1} + \sum_{k \mathop = 1}^{s + 1} \tuple {n + k, m + k - 1}$
=== Induction Step ===
This is our induction step:
So $\map P s \implies \map P {s + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds \forall r \in \N_{>0}: \tuple {n, m} = \tuple {n + r, m + r} + \sum_{k \mathop = 1}^r \tuple {n + k, m + k - 1}$
Category:Leibniz Harmonic Triangle
Category:Element of Leibniz Harmonic Triangle as Sum of Elements on Diagonal from Below
Element of Leibniz Harmonic Triangle is Sum of Numbers Below

== Theorem ==
The elements in the Leibniz harmonic triangle are the sum of the elements immediately below them.
== Proof ==
By definition of Leibniz harmonic triangle, element $\tuple {n, m}$ is:
:$\dfrac 1 {\paren {n + 1} \binom n m}$
Thus we have:
Hence the result.
== Sources ==
* : $35$
* : $35$
Category:Leibniz Harmonic Triangle
Element of Localization of Module is Represented as Quotient over S

== Theorem ==
Let $A$ be a commutative ring with unity.
Let $S \subseteq A$ be a multiplicatively closed subset.
Let $S^{-1}A$ be the localization of $A$ at $S$.
Let $M$ be a $A$-module.
Let $\struct { S^{-1}M, \iota}$ be the localization of $M$ at $S$.
Let $x \in S^{-1}M$.
Then there exist $m \in M$ and $s \in S$ such that:
:$x = s^{-1} \map \iota m$
== Proof ==
Recall that $S \subseteq \paren {S^{-1}A}^\times$ by .
Category:Commutative Algebra
Element of Matroid Base and Circuit has Substitute

== Theorem ==
Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $B \subseteq S$ be a base of $M$.
Let $C \subseteq S$ be a circuit of $M$.
Let $x \in B \cap C$.
Then:
:$\exists y \in C \setminus B : \paren{B \setminus \set x} \cup \set y$ is a base of $M$
That is, there exists $y \in C \setminus B$ such that substituting $y$ for $x$ in $B$ is another base.
== Proof ==
By definition of a circuit we have:
=== Lemma 1 ===
From Independent Subset of Matroid is Augmented by Base:
:$\exists X \subseteq B \setminus \paren{C \setminus \set x} : \paren{C \setminus \set x} \cup X$ is a base of $M$
By definition of independent and dependent subsets we have:
=== Lemma 2 ===
 
 
From matroid axiom $(\text I 4)$ we have:
=== Lemma 3 ===
 
 
From Independent Subset is Base if Cardinality Equals Cardinality of Base:
:$\paren {B \setminus \set x} \cup \set y$ is a base of $M$
Because $x \notin \paren {C \setminus \set x} \cup X$:
:$y \ne x$
By definition of set difference:
:$y \notin B \setminus \set x$:
By definition of set union:
:$y \notin \paren {B \setminus \set x} \cup \set x = B$
By the definition of a subset:
:$y \notin X$
By definition of set union:
:$y \in C \setminus \set x \subseteq C$
By definition of set difference:
:$y \in C \setminus B$
Category:Matroid Bases
Category:Matroid Circuits
Category:Element of Matroid Base and Circuit has Substitute
Element of Matroid Base and Circuit has Substitute/Lemma 1

== Lemma for Element of Matroid Base and Circuit has Substitute ==
Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $B \subseteq S$ be a base of $M$.
Let $C \subseteq S$ be a circuit of $M$.
Let $x \in B \cap C$.
Then:
:$C \setminus \set x$ is an independent proper subset of $C$
== Proof ==
By definition of circuit:
:$C$ is a minimal dependent subset of $S$
From Singleton of Element is Subset:
:$\set x \subseteq C$ and $\set x \subseteq B$
From matroid axiom $(\text I 2)$:
:$\set x \in \mathscr I$
Because $C \notin \mathscr I$:
:$\set x \ne C$
Hence:
:$\set x \subsetneq C$
From Set Difference with Non-Empty Proper Subset is Non-Empty Proper Subset:
:$C \setminus \set x$ is a proper subset of $C$
As $C$ is a minimal dependent subset:
:$C \setminus \set x \in \mathscr I$
Category:Element of Matroid Base and Circuit has Substitute
Element of Matroid Base and Circuit has Substitute/Lemma 2

== Lemma for Element of Matroid Base and Circuit has Substitute ==
Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $C \subseteq S$ be a dependent subset of $M$.
Let $x \in C$.
Let $X \subseteq S$ such that:
:$\paren {C \setminus \set x} \cup X \in \mathscr I$
Then:
:$x \notin \paren {C \setminus \set x} \cup X$
== Proof ==
:
:$x \in \paren {C \setminus \set x} \cup X$
Then:
:$\set x, C \setminus \set x \subseteq \paren {C \setminus \set x} \cup X$
From Union of Subsets is Subset:
:$C \subseteq \paren {C \setminus \set x} \cup X$
From matroid axiom $(\text I 2)$:
:$C \in \mathscr I$
This contradicts:
:$C \notin \mathscr I$
It follows that:
:$x \notin \paren {C \setminus \set x} \cup X$
Category:Element of Matroid Base and Circuit has Substitute
Element of Matroid Base and Circuit has Substitute/Lemma 3

== Lemma for Element of Matroid Base and Circuit has Substitute ==
Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $B \subseteq S$ be a base of $M$.
Let $C \subseteq S$ be a circuit of $M$.
Let $x \in B \cap C$.
Let $X \subseteq S$ such that:
:$\paren{ C \setminus \set x} \cup X$ is a base of $M$.
Then:
:$\exists y \in \paren {\paren {C \setminus \set x} \cup X} \setminus \paren {B \setminus \set x} : \paren {B \setminus \set x} \cup \set y \in \mathscr I : \card {\paren {B \setminus \set x} \cup \set y} = \card {\paren {C \setminus \set x} \cup X}$
== Proof ==
 
From Set Difference is Subset:
:$B \setminus \set x \subseteq B$
From matroid axiom $(\text I 2)$:
:$B \setminus \set x \in \mathscr I$
We have
From matroid axiom $(\text I 3')$:
:$\exists y \in \paren {\paren {C \setminus \set x} \cup X} \setminus \paren {B \setminus \set x} : \paren {B \setminus \set x} \cup \set y \in \mathscr I : \card {\paren {B \setminus \set x} \cup \set y} = \card {\paren {C \setminus \set x} \cup X}$
Category:Element of Matroid Base and Circuit has Substitute
Element of Minimally Inductive Set is Transitive Set

== Theorem ==
Let $\omega$ be the minimally inductive set.
Let $n \in \omega$.
Then $x \in n \implies x \subseteq n$.
That is, every element of $n$ is also a subset of it.
In other words, each element of $\omega$ is a transitive set.
== Proof ==
Let $S \subseteq$ be the set of all transitive elements of $\omega$.
That is:
:$n \in S \iff n \in \omega \land \forall x \in n: x \subseteq n$
It is vacuously true that $0 \in S$, as there are no $x \in 0$.
Now suppose $n \in S$.
If $x \in n^+$ then either $x \in n$ or $x = n$.
In the first case:
:$x \subseteq n$ as $n \in S$
and so:
:$x \subseteq n^+$
In the second case, by definition of successor set:
:$x \subseteq n^+$
By Principle of Mathematical Induction for Minimally Inductive Set it follows that:
:$S = \omega$
Hence the result.
== Sources ==
* : $\S 12$: The Peano Axioms
Category:Minimally Inductive Set