nyuuzyou/wikis huggingface dataset:
Existence of Unique Subsemigroup Generated by Subset/Proof 1

== Theorem ==
== Proof ==
=== Existence ===
First, we prove that such a subsemigroup exists.
Let $\mathbb S$ be the set of all subsemigroups of $S$ which contain $X$.
$\mathbb S \ne \O$ because $S$ is itself a subsemigroup of $S$ (trivial), and thus $S \in \mathbb S$.
Let $T$ be the intersection of all the elements of $\mathbb S$.
By Intersection of Subsemigroups, $T$ is the largest element of $\mathbb S$ contained in each element of $\mathbb S$.
Thus $T$ is a subsemigroup of $S$.
Since $\forall x \in \mathbb S: X \subseteq x$, we see that $X \subseteq T$, so $T \in \mathbb S$.
=== Smallest ===
Now to show that $T$ is the smallest such subsemigroup.
If any $K \le S: X \subseteq K$, then $K \in \mathbb S$ and therefore $T \subseteq K$.
So $T$ is the smallest subsemigroup of $S$ containing $X$.
=== Uniqueness ===
Now we show that $T$ is unique.
Suppose $\exists T_1, T_2 \in \mathbb S$ such that $T_1$ and $T_2$ were two such smallest subsemigroups containing $X$.
Then, by the definition of smallest, each would be equal in size.
, suppose that $T_1$ is not a subset of $T_2$.
Then their intersection (by definition containing $X$) would be a subsemigroup smaller than $T_1$.
Hence $T_1$ would not be the smallest.
Therefore each must be the subset of each other.
By definition of set equality, they must be the same set.
So the smallest subsemigroup, whose existence we have proved above, is unique.
Category:Existence of Unique Subsemigroup Generated by Subset
Existence of Unique Subsemigroup Generated by Subset/Proof 2

== Theorem ==
== Proof ==
Let $\mathbb S$ be the set of all subsemigroups of $S$.
From Set of Subsemigroups forms Complete Lattice:
:$\struct {\mathbb S, \subseteq}$ is a complete lattice.
where for every set $\mathbb H$ of subsemigroups of $S$:
:the infimum of $\mathbb H$ necessarily admitted by $\mathbb H$ is $\ds \bigcap \mathbb H$.
Hence the result, by definition of infimum.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings: Exercise $14.12$
Category:Existence of Unique Subsemigroup Generated by Subset
Existence of Universal Class

== Theorem ==
There exists a unique class $V$ such that:
:$\forall u: u \in V$
That is, the universal class exists and is unique.
== Proof ==
By Existence of Empty Class, there is a unique class $\O$ such that:
:$\forall u: u \notin \O$
for every set $u$.
Thus, by Existence of Class Complement, there is a unique class $\overline \O$ such that:
:$u \in \overline \O \iff u \notin \O$
But then, by the definition of $\O$:
:$\forall u: u \in \overline \O$
Then, $V := \overline \O$ satisfies the theorem, and is unique.
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
Existence of Upper Bound of Finite Subset of Directed Set

== Theorem ==
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\FF \subseteq \Lambda$ be a finite subset.
Then $\FF$ has an upper bound in $\struct {\Lambda, \preceq}$.
== Proof ==
We induct on the cardinality of $\FF$.
Let $n \in \Z_{\ge 0}$.
For all $m \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:if $\FF \subseteq \Lambda$ has $\card \FF = n$, then $\FF$ has an upper bound.
=== Basis for the Induction ===
The case $n = 0$ is vacuously true.
If $n = 1$ and $\FF = \set \lambda$, $\lambda$ is clearly an upper bound for $\FF$ in $\struct {\Lambda, \preceq}$. 
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:if $\FF \subseteq \Lambda$ has $\card \FF = k$, then $\FF$ has an upper bound.
Then we need to show:
:if $\FF \subseteq \Lambda$ has $\card \FF = k + 1$, then $\FF$ has an upper bound.
=== Induction Step ===
This is our induction step.
Let $\FF = \set {\lambda_1, \ldots, \lambda_{k + 1} }$.
Then $\GG = \set {\lambda_1, \ldots, \lambda_k}$ has $\card \GG = k$, and so there exists $\lambda \in \Lambda$ such that: 
:$\lambda_i \preceq \lambda$ for each $1 \le i \le n$.
From the definition of a directed set, there exists $\lambda_\ast \in \Lambda$ such that: 
:$\lambda \preceq \lambda_\ast$
and:
:$\lambda_{k + 1} \preceq \lambda_\ast$ 
Then we have, from transitivity:
:$\lambda_i \preceq \lambda_\ast$ for each $1 \le i \le k + 1$.
Category:Order Theory
Existence of Upper and Lower Numbers of Cut whose Difference equal Given Rational

== Theorem ==
Let $\alpha$ be a cut.
Let $r \in \Q_{>0}$ be a (strictly) positive rational number.
Then there exist rational numbers $p$ and $q$ such that:
:$p \in \alpha, q \notin \alpha$
:$q - p = r$
such that $q$ is not the smallest upper number of $\alpha$.
== Proof ==
Let $s \in \alpha$ be a rational number.
For $n = 0, 1, 2, \ldots$ let $s_n = s + n r$.
Then there exists a unique integer $m$ such that:
:$s_m \in \alpha$
and:
:$s_{m + 1} \notin \alpha$
If $s_{m + 1}$ is not the smallest upper number of $\alpha$, take:
:$p = s_m$
:$q = s_{m + 1}$
If $s_{m + 1}$ is the smallest upper number of $\alpha$, take:
:$p = s_m + \dfrac r 2$
:$q = s_{m + 1} + \dfrac r 2$
The result follows.
== Sources ==
* : Chapter $1$: The Real and Complex Number Systems: Dedekind Cuts: $1.15$. Theorem
Category:Cuts
Existence of Urysohn Function does not guarantee Normal Space

== Theorem ==
Let $T = \struct {S, \tau}$ be a regular space.
Let $T$ have the property that:
:For all closed sets $A, B \subseteq S$ of $T$ such that $A \cap B = \O$, there exists an Urysohn function for $A$ and $B$.
Then it is not necessarily the case that $T$ is a normal space.
== Proof ==
Let $T$ have the specified property.
By definition of a normal space, for $T$ to be normal, it has to be both $T_4$ space and a $T_1$ space.
From Urysohn's Lemma Converse, $T$ is a $T_4$ space.
It remains to be shown that $T$ is not necessarily a $T_1$ space.
This is done by Proof by Counterexample:
Let $S$ be a set and let $\PP$ be a partition on $S$ which is specifically not the (trivial) partition of singletons.
Let $T = \struct {S, \tau}$ be the partition space whose basis is $\PP$.
From Partition Topology is $T_4$, we have that $T$ is a $T_4$ space.
From Urysohn's Lemma, for all $A, B \subseteq S$ be closed sets of $T$ such that $A \cap B = \O$, there exists an Urysohn function for $A$ and $B$.
From Partition Topology is not $T_1$, $T$ is not a $T_1$ space.
The result follows.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Completely Regular Spaces
Category:Normal Spaces
Category:Urysohn Functions
Existence of Vitali Set implies Subset of Unit Interval with Inner Measure Zero and Outer Measure 1

== Theorem ==
Let us posit the existence of a Vitali set.
Then there exists a subset of the closed unit interval which has an inner measure of $0$ and an outer measure of $1$.
== Proof ==
== Sources ==
* : $1.$ Introduction: $1.4$ Problems: $4$
Category:Vitali Sets
Existence of Weakly Countably Compact Space which is not Countably Compact

== Theorem ==
There exists at least one example of a weakly countably compact topological space which is not also a countably compact space.
== Proof ==
Let $T$ be the deleted integer topological space.
From Deleted Integer Topology is Weakly Countably Compact, $T$ is a weakly countably compact space.
From Deleted Integer Topology is not Countably Compact, $T$ is not a countably compact space.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Global Compactness Properties
Category:Weakly Countably Compact Spaces
Category:Countably Compact Spaces
Existence of Weakly Locally Compact Space which is not Strongly Locally Compact

== Theorem ==
There exists at least one example of a weakly locally compact topological space which is not also a strongly locally compact space.
== Proof 1 ==
== Proof 2 ==
== Also see ==
* Weakly Locally Compact Hausdorff Space is Strongly Locally Compact
Category:Weakly Locally Compact Spaces
Category:Strongly Locally Compact Spaces
Category:Existence of Weakly Locally Compact Space which is not Strongly Locally Compact
Existence of Weakly Locally Compact Space which is not Strongly Locally Compact/Proof 1

== Theorem ==
== Proof ==
Let $T$ be the nested interval topological space.
From Nested Interval Topology is Weakly Locally Compact, $T$ is a weakly locally compact space.
From Nested Interval Topology is not Strongly Locally Compact, $T$ is not a strongly locally compact space.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Localized Compactness Properties
Category:Existence of Weakly Locally Compact Space which is not Strongly Locally Compact
Existence of Weakly Locally Compact Space which is not Strongly Locally Compact/Proof 2

== Theorem ==
== Proof ==
Let $T$ be an infinite particular point space.
From Particular Point Space is Weakly Locally Compact, $T$ is a weakly locally compact space.
From Infinite Particular Point Space is not Strongly Locally Compact, $T$ is not a strongly locally compact space.
Hence the result.
Category:Existence of Weakly Locally Compact Space which is not Strongly Locally Compact
Existence of Weakly Sigma-Locally Compact Space which is not Strongly Locally Compact

== Theorem ==
There exists at least one example of a weakly $\sigma$-locally compact topological space which is not also a strongly locally compact space.
== Proof ==
Let $T$ be the nested interval topological space.
From Nested Interval Topology is Weakly $\sigma$-Locally Compact, $T$ is a weakly $\sigma$-locally compact space.
From Nested Interval Topology is not Strongly Locally Compact, $T$ is not a strongly locally compact space.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Localized Compactness Properties
Category:Strongly Locally Compact Spaces
Category:Weakly Sigma-Locally Compact Spaces
Existence of n such that M - 2^n or M + 2^n has no Prime factors less than 331

== Theorem ==
Let $M \in \Z$ be an integer.
Then there exists a positive integer $n \in \Z_{\ge 0}$ such that either $M - 2^n$ or $M + 2^n$ has no prime factors less than $331$.
== Proof ==
== Sources ==
* 
* : $331$
* : $331$
Category:Not Every Number is the Sum or Difference of Two Prime Powers
Category:331
Existence of q for which j - qk is Positive

== Theorem ==
Let $j, k \in \Z$ be integers such that $k > 0$.
Then there exist $q \in \Z$ such that $j - q k > 0$.
== Proof ==
Let $q = -\size j - 1$.
Then:
We have that:
:$\forall j \le 0: j + \size j = 0$
and:
:$\forall j > 0: j + \size j = 2 j$
So:
:$j - q k \ge k$
and as $k > 0$ the result follows.
== Sources ==
* : $\text {2-1}$ Euclid's Division Lemma: Exercise $1$
Category:Number Theory
Existential Generalisation

== Theorem ==
=== Informal Statement ===
=== Existential Generalisation in Models ===
=== Existential Generalisation in Proof Systems ===
== Also known as ==
Some authors call this the Rule of Existential Introduction and it is then abbreviated $\text {EI}$.
However, beware the fact that other authors use $\text {EI}$ to abbreviate the Rule of Existential Instantiation which is the antithesis of this one.
So make sure you know exactly what terminology is specified.
Category:Predicate Logic
Existential Generalisation/Informal Statement

== Theorem ==
:$\map P {\mathbf a} \vdash \exists x: \map P x$
Suppose we have the following:
:We can find an arbitrary object $\mathbf a$ in our universe of discourse which has the property $P$.
Then we may infer that:
:there exists in that universe at least one object $x$ which has that property $P$.
This is called the Rule of Existential Generalisation and often appears in a proof with its abbreviation $\text {EG}$.
== Sources ==
* : $\S \text{IV}$: The Logic of Predicates $(2): \ 3$: Existential Propositions
Category:Predicate Logic
Existential Generalisation/Model

== Theorem ==
Let $\map {\mathbf A} x$ be a WFF of predicate logic.
Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.
Then $\map {\mathbf A} \tau \implies \exists x: \map {\mathbf A} x$ is a tautology.
== Proof ==
Let $\AA$ be a structure on a set $A$, and let $\sigma$ be an assignment for $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$.
Define:
:$a_\tau := \map {\operatorname{val}_\AA} \tau \sqbrk \sigma$
the value of $\tau$ under $\sigma$.
From the definition of value under $\sigma$:
:$\map {\operatorname{val}_\AA} {\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau} \sqbrk \sigma = \map {f^\to} {\map {\operatorname{val}_\AA} {\forall x: \map {\mathbf A} x} \sqbrk \sigma, \map {\operatorname{val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma}$
where $f^\to$ is the truth function of $\implies$.
We thus need to ascertain that if:
:$\map {\operatorname{val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma = \T$
then also:
:$\map {\operatorname{val}_\AA} {\exists x: \map {\mathbf A} x} \sqbrk \sigma = \T$
By the Substitution Theorem for Well-Formed Formulas, the former amounts to:
:$\map {\operatorname{val}_\AA} {\map {\mathbf A} x} \sqbrk {\sigma + \paren {x / a_\tau} } = \T$
By the definition of value under $\sigma$, the latter reduces to:
:$\map {\operatorname{val}_\AA} {\map {\mathbf A} x} \sqbrk {\sigma + \paren {x / a} } = \T$
for some $a \in A$.
Since $a_\tau \in A$, the conclusion follows, and $\map {\mathbf A} \tau \implies \exists x: \map {\mathbf A} x$ is a tautology.
== Sources ==
* : $\text{II}.8$ Further Semantic Notions: Corollary $\text{II.8.12}$
Category:Predicate Logic
Existential Generalisation/Proof System

== Theorem ==
Let $\map {\mathbf A} x$ be a WFF of predicate Logic of $\LL$.
Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.
Let $\mathscr H$ be Hilbert proof system instance 1 for predicate logic.
Then:
:$\map {\mathbf A} \tau \vdash_{\mathscr H} \exists x: \map {\mathbf A} x$
is a provable consequence in $\mathscr H$.
== Proof ==
== Sources ==
* : $\text{II}.11$ Some Strategies for Constructing Proofs: Lemma $\text{II}.11.8$: Quantifier Rules (result statement)
Category:Predicate Logic
Category:Hilbert Proof System Instance 1 for Predicate Logic
Existential Instantiation/Informal Statement

== Theorem ==
:$\exists x: \map P x, \map P {\mathbf a} \implies y \vdash y$
Suppose we have the following:
:From our universe of discourse, any arbitrarily selected object $\mathbf a$ which has the property $P$ implies a conclusion $y$
:$\mathbf a$ is not free in $y$
:It is known that there does actually exists an object that has $P$.
Then we may infer $y$.
This is called the Rule of Existential Instantiation and often appears in a proof with its abbreviation $\text {EI}$.
When using this rule of existential instantiation:
:$\exists x: \map P x, \map P {\mathbf a} \implies y \vdash y$
the instance of $\map P {\mathbf a}$ is referred to as the typical disjunct.
== Proof ==
This is an extension of Proof by Cases.
The propositional expansion of $\exists x: \map P x$ is:
:$\map P {\mathbf X_1} \lor \map P {\mathbf X_2} \lor \map P {\mathbf X_3} \lor \ldots$
We know that any arbitrarily selected $\mathbf a$ with the property $P$ implies $y$.
From this we can infer that all such $\mathbf a$ which have that property imply $y$.
This is equivalent to the step in Proof by Cases in which we need to prove that both disjuncts lead to the same conclusion.
The fact that we only need one of them in fact to be true is quite enough to draw the conclusion that $y$ is true.
In this context, we are assured by the statement $\exists x: \map P x$ that at least one such disjunct in the above propositional expansion is true.
Thus the conclusion follows, and the result is proved.
== Sources ==
* : $\S \text{IV}$: The Logic of Predicates $(2): \ 3$: Existential Propositions
Category:Predicate Logic
Existential Instantiation/Proof System

== Theorem ==
Let $\LL$ be a specific signature for the language of predicate logic.
Let $\mathscr H$ be Hilbert proof system instance 1 for predicate logic.
Let $\map {\mathbf A} x, \mathbf B$ be WFFs of $\LL$.
Let $\FF$ be a collection of WFFs of $\LL$.
Let $c$ be an arbitrary constant symbol which is not in $\LL$.
Let $\LL'$ be the signature $\LL$ extended with the constant symbol $c$.
Suppose that we have the provable consequence (in $\LL'$):
:$\FF, \map {\mathbf A} c \vdash_{\mathscr H} \mathbf B$
Then we may infer (in $\LL$):
:$\FF, \exists x: \map {\mathbf A} x \vdash_{\mathscr H} \mathbf B$
== Proof ==
== Sources ==
* : $\text{II}.11$ Some Strategies for Constructing Proofs: Lemma $\text{II}.11.8$: Quantifier Rules (result statement)
Category:Predicate Logic
Category:Hilbert Proof System Instance 1 for Predicate Logic
Existential Quantification of Provable Arithmetic Formula is Provable

== Theorem ==
Let $\map \phi x$ be a WFF in the language of arithmetic with $1$ free variable.
Let $\sqbrk a$ denote the unary representation of $a$.
Suppose that, for every $n \in \N$ such that $\N \models \map \phi {x \gets \sqbrk n}$:
:$\map \phi {x \gets \sqbrk n}$
is a theorem of minimal arithmetic.
Suppose also that:
:$\N \models \exists x: \map \phi x$
Then:
:$\exists x: \map \phi x$
is a theorem of minimal arithmetic.
== Proof ==
By definition of value of formula:
:$\exists x \in \N: \map \phi x$
Choose $x_0 \in \N$ that satisfies $\map \phi {x \gets x_0}$.
By Unary Representation of Natural Number:
:$x_0 = \sqbrk {x_0}$
Thus, by Substitution Property of Equality:
:$\map \phi {x \gets \sqbrk {x_0} }$
But then, by hypothesis:
:$\map \phi {x \gets \sqbrk {x_0} }$
is a theorem of minimal arithmetic.
The result follows from Existential Generalisation.
Category:Natural Numbers
Category:Proof Theory
Existential Quantifier Distributes over Conjunction

== Theorem ==
Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.
Then:
:$\exists x: \paren {\map \phi x \land \map \psi x} \vdash \paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}$
== Proof ==
Category:Existential Quantifier
Existential Quantifier Distributes over Disjunction

== Theorem ==
Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.
Then:
:$\exists x: \paren {\map \phi x \lor \map \psi x} \dashv \vdash \paren {\exists x: \map \phi x} \lor \paren {\exists x: \map \psi x}$
== Proof ==
=== Forward Implication ===
=== Reverse Implication ===
Category:Existential Quantifier
Existential Statement/Examples/Some Men are Mortal

== Example of Existential Statement ==
The statement:
:Some men are mortal
is an example of an existential statement.
It is expressed explicitly as:
:There exists at least one man who is mortal
and has the logical form:
:$\exists x: \map {\operatorname {Mortal} } x$
where:
:the universal set is implicitly assumed to be the set of all men
:$\operatorname {Mortal}$ is the predicates is mortal.
== Sources ==
* 
* 
Category:Examples of Existential Statements
Exists Bijection to a Disjoint Set

== Theorem ==
Let $S$ and $T$ be sets.
Then there exists a bijection from $T$ onto a set $T'$ disjoint from $S$.
== Proof ==
Consider the set:
:$X = \text{Ran}(S) = \set {y: \paren {\exists x : \tuple {x, y} \in S} }$
From Relation is Set implies Domain and Image are Sets, this is indeed a set.
That is, $X$ consists of all the elements which are the second coordinate of some ordered pair which happens to be in $S$.
From Exists Element Not in Set, we have that $\exists z: z \notin X$.
Now consider the cartesian product $T' = T \times \set z$.
Suppose that $p \in T'$.
Then $p = \tuple {c, z}$ where $c \in T$.
Suppose $\tuple {c, z} \in S$.
Then that would mean that $z \in X$.
But we have specifically selected $z$ such that $z \notin X$.
So $p = \tuple {c, z} \notin S$.
Thus we have that $T' \cap S = \O$.
There is an obvious bijection $g: T \to T'$:
:$\forall t \in T: \map g t = \tuple {t, z}$
and hence the result.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 8$: Compositions Induced on Subsets
* : Chapter $\text {II}$: New Structures from Old: $\S 8$: Compositions Induced on Subsets: Exercise $8.12$
Category:Bijections
Category:Disjoint Sets
Exists Divisor in Set of n+1 Natural Numbers no greater than 2n

== Theorem ==
Let $S$ be a set of $n + 1$ non-non-zero natural numbers all less than or equal to $2 n$.
Then there exists $a, b \in S$ such that
:$a \divides b$
where $\divides$ denotes divisibility.
== Proof ==
Let $\alpha$ denote the relation defined on the natural numbers $\N$ by:
:$\forall x, y \in \N: x \mathrel \alpha y \iff \exists n \in \Z: x = 2^n y$
From Equivalence Relation on Natural Numbers such that Quotient is Power of Two, $\alpha$ is an equivalence relation.
From Equivalence Class under $\alpha$ Contains $1$ Odd Number, each odd integer between $1$ and $2 n$ is in its own equivalence class.
Each even integer $m$ between $1$ and $2 n$ is equal to an odd integer $p$ strictly less than $m$ multiplied by a power of $2$.
Hence each such $m$ is an element of one of the equivalence classes of one of the $n$ odd integers between $1$ and $2 n$.
Thus each element of $S$ is an element of one of exactly $n$ equivalence classes of $\alpha$.
But there are $n + 1$ elements of $S$.
So by the Pigeonhole Principle, at least $2$ elements of $S$ are in the same equivalence class.
Thus let $a, b \in S: a \mathrel \alpha b$.
From One of Pair of Equivalent Elements is Divisor of the Other, either $a \divides b$ or $b \divides a$.
Hence the result.
== Sources ==
* : $\S 6$. Indexed families; partitions; equivalence relations: Exercise $8$
Category:Divisibility
Exists Element Not in Set/Proof 1

== Theorem ==
== Proof ==
Consider the power set $\powerset S$ of $S$.
 $\forall x \in \powerset S: x \in S$.
Then the identity mapping $I_S: S \to \powerset S$ would be a surjection.
But from Cantor's Theorem, there is no surjection $f: S \to \powerset S$.
From this contradiction it follows that:
:$\exists x \in \powerset S: x \notin S$
Hence the result.
Category:Exists Element Not in Set
Exists Element Not in Set/Proof 2

== Theorem ==
== Proof ==
By Axiom of Specification, we can construct the set:
:$T = \set {x \in S: x \notin x}$
Then for all $y$:
:$(*) \quad y \in T$ $\paren {y \in S \land y \notin y}$.
 $T \in S$.
By Law of Excluded Middle, either $T \in T$ or $T \notin T$.
Suppose $T \in T$.
By $(*)$, $T \in S \land T \notin T$.
By Rule of Simplification we have $T \notin T$, which is a contradiction.
Now suppose $T \notin T$.
By $(*)$ again, we have $\neg \paren {T \in S \land T \notin T}$.
By Modus Ponendo Tollens, $\neg \paren {T \in S}$, which is also a contradiction.
Hence we must have $T \notin S$.
And thus there exists something (namely $T$) that does not belong to $S$.
== Sources ==
* : $\S 2$: The Axiom of Specification
Category:Exists Element Not in Set
Exists Ordinal Greater than Set of Ordinals

== Theorem ==
Let $S$ be a set of ordinals.
Then there exists an ordinal greater than every element of $S$:
:If $S$ contains a greatest ordinal $\alpha$, then $\alpha^+$ is greater than every element of $S$
:If $S$ does not contain a greatest ordinal, then $\bigcup S$ is greater than every element of $S$.
== Proof ==
Recall that Class of All Ordinals is Well-Ordered by Subset Relation.
Suppose $S$ contains a greatest ordinal $\alpha$.
Because $\alpha^+$ is greater than $\alpha$ by definition, it follows that $\alpha^+$ is greater than every element of $S$.
Suppose $S$ does not contain a greatest ordinal.
Consider the union $\bigcup S$ of $S$.
If $\bigcup S \in S$ it would be the greatest element of $S$.
Hence $\bigcup S \notin S$.
Let $\alpha \in S$.
Then:
:$\alpha \ne \bigcup S$
But:
:$\alpha \subseteq \bigcup S$
and so:
:$\alpha \subsetneqq S$
From Union of Set of Ordinals is Ordinal, $\bigcup S$ is an ordinal.
Hence by definition of the usual ordering on ordinals:
:$a < \bigcup S$
Thus $\bigcup S$ is greater than every element of $S$.
Hence the result.
== Sources ==
* : Chapter $5$: Ordinal Numbers: $\S 1$ Ordinal numbers: Theorem $1.18$
Category:Ordinals