avewright/proofwiki-math huggingface dataset:
Theorem: Principle of Recursive Definition

Let $\N$ be the natural numbers.
Let $T$ be a class (which may be a set).
Let $a \in T$.
Let $g: T \to T$ be a mapping.
Then there exists exactly one mapping $f: \N \to T$ such that:
:<nowiki>$\forall x \in \N: \map f x = \begin{cases}
a & : x = 0 \\
\map g {\map f n} & : x = n + 1
\end{cases}$</nowiki>

Proof:
Consider $\N$, defined as a naturally ordered semigroup $\struct {S, \circ, \preceq}$.
Let the mapping $f$ be defined as:
:<nowiki>$\map f x = \begin{cases}
a & : x = 0 \\
\map s {\map f n} & : x = n \circ 1 \end{cases}$</nowiki>
if $\map f n$ is defined.
Let $S' = \set {n \in S: \map f n \text{ is defined} }$.
Then:
:$0 \in S'$
and:
:$n + 1 \in S'$
so by Principle of Mathematical Induction for Naturally Ordered Semigroup:
:$S' = S$
Thus the domain of $f$ is $S$.
Consequently, $f$ is a mapping from $S$ into $T$ which satisfies:
:$\map f 0 = a$
and:
:$\map f {n \circ 1} = \map s {\map f n}$
for all $n \in S$.
{{qed}}
=== Objections ===
$(1):$
In the above argument, $S'$ is not precisely defined.
In order for a set to be defined, that definition should be able to be expressed solely in terms of logic and definitions from set theory.
In this case, the expression "is defined" does not meet that criterion.
$(2):$
The mapping $f$ is not defined properly.
A mapping needs to be defined as a set of ordered pairs which needs to satisfy a condition.
In the above, it is indeed specified that
:$\tuple {0, a} \in f$
and:
:$\tuple {n \circ 1, \map s x} \in f$ whenever $\tuple {n, x} \in f$
Thus it appears either that:
:$f$ itself is used to define $f$
or else that:
:$f$ itself changes during the process in which it is being defined.
Neither of these possibilities can be accepted.
$(3):$
The only property of $\struct {S, \circ, \preceq}$ used in the argument is that it satisfies Principle of Mathematical Induction for Naturally Ordered Semigroup.
However, consider the commutative semigroup $\struct {D, +}$ which has elements $0$ and $1$, such that:
:$D$ is the only subset of $D$:
::containing $0$
:and
::containing $x + 1$ whenever it contains $x$.
Then:
:for any set $T$
:any mapping $g: T \to T$
:any element $a \in T$
there exists a mapping $f: D \to T$ such that:
:<nowiki>$\map f y = \begin{cases}
a & : y = 0 \\
\map s {\map f x} & : y = x + 1 \end{cases}$</nowiki>
But consider the additive group of integers modulo $2$:
:$\struct {\Z_2, +_2}$
which is indeed a commutative semigroup containing $0$ and $1$ which satisfies the hypothesis.
But if $g: \N \to \N$ is the mapping defined as:
:$\map g n = n + 1$
there is no mapping $f: \Z_2 \to \N$ which satisfies:
:<nowiki>$\map f y = \begin{cases}
0 & : y = 0 \\
\map s {\map f x} & : y = x +_2 1 \end{cases}$</nowiki>
for all $x \in \Z_2$.
Hence the argument is invalid.
Theorem: Principle of Recursive Definition

Let $\N$ be the natural numbers.
Let $T$ be a class (which may be a set).
Let $a \in T$.
Let $g: T \to T$ be a mapping.
Then there exists exactly one mapping $f: \N \to T$ such that:
:<nowiki>$\forall x \in \N: \map f x = \begin{cases}
a & : x = 0 \\
\map g {\map f n} & : x = n + 1
\end{cases}$</nowiki>

Proof:
Consider $\N$ defined as a Peano structure $\struct {P, 0, s}$.
The result follows from Principle of Recursive Definition for Peano Structure.
{{qed}}
Theorem: Principle of Recursive Definition

Let $\N$ be the natural numbers.
Let $T$ be a class (which may be a set).
Let $a \in T$.
Let $g: T \to T$ be a mapping.
Then there exists exactly one mapping $f: \N \to T$ such that:
:<nowiki>$\forall x \in \N: \map f x = \begin{cases}
a & : x = 0 \\
\map g {\map f n} & : x = n + 1
\end{cases}$</nowiki>

Proof:
Consider $\N$ defined as the von Neumann construction of the natural numbers.
The result follows from Principle of Recursive Definition for Minimally Inductive Set.
{{qed}}
Theorem: Principle of Recursive Definition

Let $\N$ be the natural numbers.
Let $T$ be a class (which may be a set).
Let $a \in T$.
Let $g: T \to T$ be a mapping.
Then there exists exactly one mapping $f: \N \to T$ such that:
:<nowiki>$\forall x \in \N: \map f x = \begin{cases}
a & : x = 0 \\
\map g {\map f n} & : x = n + 1
\end{cases}$</nowiki>

Proof:
Recall the general result:
{{:Principle of Recursive Definition/General Result}}
The result follows from setting $p = 0$.
{{qed}}
Theorem: Principle of Recursive Definition

Let $\N$ be the natural numbers.
Let $T$ be a class (which may be a set).
Let $a \in T$.
Let $g: T \to T$ be a mapping.
Then there exists exactly one mapping $f: \N \to T$ such that:
:<nowiki>$\forall x \in \N: \map f x = \begin{cases}
a & : x = 0 \\
\map g {\map f n} & : x = n + 1
\end{cases}$</nowiki>

Proof:
From the Principle of Recursive Definition: Strong Version:
{{:Principle of Recursive Definition/Strong Version}}
Let $h: A \to A$ be defined as:
:$\forall x \in A: \map h x := \map g {a, x}$ for arbitrary $a \in \omega$
That is:
:$\forall y \in \omega: \map g {y, x} = \map h x$
Then {{apriori}} there exists exactly one mapping $f: \omega \to A$ such that:
:<nowiki>$\forall x \in \omega: \map f x = \begin {cases}
c & : x = \O \\
\map h {\map f n} & : x = n^+
\end {cases}$</nowiki>
The result follows on identifying $\omega$ with $\N$, $c$ with $a$, $A$ with $T$, $\O$ with $0$ and $n^+$ with $n + 1$.
{{qed}}
Theorem: Principle of Recursive Definition/General Result

Let $p \in \N$.
Let $p^\ge$ be the upper closure of $p$ in $\N$:
:$p^\ge := \set {x \in \N: x \ge p} = \set {p, p + 1, p + 2, \ldots}$
Then there exists exactly one mapping $f: p^\ge \to T$ such that:
:<nowiki>$\forall x \in p^\ge: \map f x = \begin{cases}
a & : x = p \\
\map g {\map f n} & : x = n + 1
\end{cases}$</nowiki>

Proof:
Consider $\N$, defined as a naturally ordered semigroup $\struct {S, \circ, \preceq}$.
For simplicity, let $S' = p^\ge$.
First an '''admissible mapping''' is defined.
Let $n \in S'$.
The mapping $h: \closedint p n \to T$ is defined as an '''admissible mapping''' for $n$ {{iff}}:
:<nowiki>$\forall r \in \closedint p n: \map h r = \begin{cases}
a & : r = p \\
\map g {\map h y} & : r = y \circ 1
\end{cases}$</nowiki>
where $\closedint p n$ denotes an integer interval of $S$:
:$\closedint p n = \set {r \in S: p \le r \le n}$
Define:
:$A = \set {x \in S': x \text { has exactly one admissible mapping} }$
We now use the Principle of Mathematical Induction for a Naturally Ordered Semigroup to prove that $A = S'$.
Theorem: Integers are not Densely Ordered

The integers $\Z$ are not densely ordered.
That is:
:$\forall n \in \Z: \not \exists m \in \Z: n < m < n + 1$

Proof:
By definition of immediate successor element, this is equivalent to the statement:
:$\forall n \in \Z: n + 1$ is the immediate successor to $n$
We have that Integers form Ordered Integral Domain.
From One Succeeds Zero in Well-Ordered Integral Domain:
:$\not \exists r \in \Z: 0 < r < 1$
From Properties of Ordered Ring:
:$a < b \implies n + a < n + b$
Putting $a = 0, b = 1, m = n + r$:
:$\not \exists m \in \Z: n + 0 < m < n + 1$
Hence the result.
{{qed}}
Theorem: Real Zero is Zero Element

:$\forall x \in \R: 0 \times x = 0$

Proof:
{{begin-eqn}}
{{eqn | l = 0 \times x
      | r = \paren {0 + 0} \times x
      | c = {{Real-number-axiom|A3}}
}}
{{eqn | r = 0 \times x + 0 \times x
      | c = {{Real-number-axiom|D}}
}}
{{eqn | ll= \leadsto
      | l = 0 \times x
      | r = 0
      | c = Real Addition Identity is Zero: Corollary
}}
{{end-eqn}}
{{qed}}
Theorem: Negative of Real Zero equals Zero

Let $0$ denote the identity for addition in the real numbers $\R$.
Then:
:$-0 = 0$

Proof:
{{begin-eqn}}
{{eqn | l = -0 + 0
      | r = 0
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = -0
      | r = 0
      | c = Real Addition Identity is Zero: Corollary
}}
{{end-eqn}}
{{qed}}
Theorem: Negative of Negative Real Number

:$\forall x \in \R: -\paren {-x} = x$

Proof:
{{begin-eqn}}
{{eqn | l = 0
      | r = \paren {-x} + x
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = -\paren {-x} + 0
      | r = -\paren {-x} + \paren {-x} + x
      | c = adding $-\paren {-x}$ to both sides
}}
{{eqn | ll= \leadsto
      | l = -\paren {-x} + 0
      | r = \paren {-\paren {-x} + \paren {-x} } + x
      | c = {{Real-number-axiom|A1}}
}}
{{eqn | ll= \leadsto
      | l = -\paren {-x} + 0
      | r = 0 + x
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = -\paren {-x}
      | r = x
      | c = {{Real-number-axiom|A3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Multiplication by Negative Real Number

:$\forall x, y \in \R: x \times \paren {-y} = -\paren {x \times y} = \paren {-x} \times y$

Proof:
{{begin-eqn}}
{{eqn | l = x \times \paren {\paren {-y} + y}
      | r = x \times 0
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | r = 0
      | c = Real Zero is Zero Element
}}
{{eqn | ll= \leadsto
      | l = \paren {x \times \paren {-y} } + \paren {x \times y}
      | r = 0
      | c = {{Real-number-axiom|D}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {x \times \paren {-y} } + \paren {x \times y} } + \paren {-\paren {x \times y} }
      | r = 0 + \paren {-\paren {x \times y} }
      | c = adding $-\paren {x \times y}$ to both sides
}}
{{eqn | ll= \leadsto
      | l = \paren {x \times \paren {-y} } + \paren {\paren {x \times y} + \paren {-\paren {x \times y} } }
      | r = 0 + \paren {-\paren {x \times y} }
      | c = {{Real-number-axiom|A1}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x \times \paren {-y} } + 0
      | r = 0 + \paren {-\paren {x \times y} }
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = x \times \paren {-y}
      | r = -\paren {x \times y}
      | c = {{Real-number-axiom|A3}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = \paren {x + \paren {-x} } \times y
      | r = 0 \times y
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | r = 0
      | c = Real Zero is Zero Element
}}
{{eqn | ll= \leadsto
      | l = \paren {x \times y} + \paren {\paren {-x} \times y}
      | r = 0
      | c = {{Real-number-axiom|D}}
}}
{{eqn | ll= \leadsto
      | l = -\paren {x \times y} + \paren {\paren {x \times y} + \paren {\paren {-x} \times y} }
      | r = -\left({x \times y}\right) + 0
      | c = adding $-\paren {x \times y}$ to both sides
}}
{{eqn | ll= \leadsto
      | l = \paren {-\paren {x \times y} + \paren {x \times y} } + \paren {\paren {-x} \times y}
      | r = -\paren {x \times y} + 0
      | c = {{Real-number-axiom|A1}}
}}
{{eqn | ll= \leadsto
      | l = 0 + \paren {\paren {-x} \times y}
      | r = -\paren {x \times y} + 0
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = \paren {-x} \times y
      | r = -\paren {x \times y}
      | c = {{Real-number-axiom|A3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Negative of Sum of Real Numbers

:$\forall x, y \in \R: -\paren {x + y} = -x - y$

Proof:
{{begin-eqn}}
{{eqn | l = -\paren {x + y}
      | r = \paren {-1} \times \paren {x + y}
      | c = {{Corollary|Multiplication by Negative Real Number}}
}}
{{eqn | r = \paren {\paren {-1} \times x} + \paren {\paren {-1} \times y}
      | c = {{Real-number-axiom|D}}
}}
{{eqn | r = \paren {-x} + \paren {-y}
      | c = {{Corollary|Multiplication by Negative Real Number}}
}}
{{eqn | r = -x - y
      | c = {{Defof|Real Subtraction}}
}}
{{end-eqn}}
{{qed}}
Theorem: Negative of Sum of Real Numbers/Corollary

:$\forall x, y \in \R: -\paren {x - y} = -x + y$

Proof:
{{begin-eqn}}
{{eqn | l = -\paren {x - y}
      | r = -\paren {x + \paren {-y} }
      | c = {{Defof|Real Subtraction}}
}}
{{eqn | r = -x - \paren {-y}
      | c = Negative of Sum of Real Numbers
}}
{{eqn | r = -x + \paren {-\paren {-y} }
      | c = {{Defof|Real Subtraction}}
}}
{{eqn | r = -x + y
      | c = Negative of Negative Real Number
}}
{{end-eqn}}
{{qed}}
Theorem: Real Multiplication Identity is One/Corollary

:$\forall x \in \R_{\ne 0}: x \times y = x \implies y = 1$

Proof:
{{begin-eqn}}
{{eqn | l = x \times y
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac 1 x \times \paren {x \times y}
      | r = \frac 1 x \times x
      | c = as long as $x \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac 1 x \times x} \times y
      | r = \frac 1 x \times x
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | ll= \leadsto
      | l = 1 \times y
      | r = 1
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = 1
      | c = Real Multiplication Identity is One
}}
{{end-eqn}}
{{qed}}
Theorem: Real Number Divided by Itself

:$\forall x \in \R_{\ne 0}: \dfrac x x = 1$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \ne 0
      | l = \frac x x
      | r = x \times \frac 1 x
      | c = {{Defof|Real Division}}
}}
{{eqn | r = 1
      | c = {{Real-number-axiom|M4}}
}}
{{end-eqn}}
{{qed}}
Theorem: Real Division by One

:$\forall x \in \R: \dfrac x 1 = x$

Proof:
{{begin-eqn}}
{{eqn | l = \frac x 1
      | r = x \times \frac 1 1
      | c = {{Defof|Real Division}}
}}
{{eqn | r = x \times 1
      | c = Real Number Divided by Itself
}}
{{eqn | r = x
      | c = {{Real-number-axiom|M4}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Reciprocals of Real Numbers

:$\forall x, y \in \R_{\ne 0}: \dfrac 1 x \times \dfrac 1 y = \dfrac 1 {x \times y}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {x \times y} \times \paren {x \times y}
      | r = 1
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {x \times y} \times \paren {x \times y} \times \frac 1 y
      | r = 1 \times \frac 1 y
      | c = as $y \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac 1 {x \times y} \times x} \times \paren {y \times \frac 1 y}
      | r = 1 \times \frac 1 y
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac 1 {x \times y} \times x} \times 1
      | r = 1 \times \frac 1 y
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {x \times y} \times x
      | r = \frac 1 y
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac 1 {x \times y} \times x} \times \frac 1 x
      | r = \frac 1 y \times \frac 1 x
      | c = as $x \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {x \times y} \times \paren {x \times \frac 1 x}
      | r = \frac 1 y \times \frac 1 x
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {x \times y} \times 1
      | r = \frac 1 y \times \frac 1 x
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {x \times y}
      | r = \frac 1 y \times \frac 1 x
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {x \times y}
      | r = \frac 1 x \times \frac 1 y
      | c = {{Real-number-axiom|M2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Quotients of Real Numbers

:$\forall x, w \in \R, y, z \in \R_{\ne 0}: \dfrac x y \times \dfrac w z = \dfrac {x \times w} {y \times z}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac x y \times \frac w z
      | r = x \times \frac 1 y \times w \times \frac 1 z
      | c = {{Defof|Real Division}}
}}
{{eqn | r = x \times w \times \frac 1 y \times \frac 1 z
      | c = {{Real-number-axiom|M2}}
}}
{{eqn | r = \paren {x \times w} \times \paren {\frac 1 y \times \frac 1 z}
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | r = \paren {x \times w} \times \frac 1 {y \times z}
      | c = Product of Reciprocals of Real Numbers
}}
{{eqn | r = \dfrac {x \times w} {y \times z}
      | c = {{Defof|Real Division}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Quotients of Real Numbers

:$\forall x, w \in \R, y, z \in \R_{\ne 0}: \dfrac x y + \dfrac w z = \dfrac {\paren {x \times z} + \paren {y \times w} } {y \times z}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac x y + \frac w z
      | r = \paren {x \times \frac 1 y} + \paren {w \times \frac 1 z}
      | c = {{Defof|Real Division}}
}}
{{eqn | r = \paren {x \times \frac 1 y \times 1} + \paren {1 \times w \times \frac 1 z}
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | r = \paren {x \times \frac 1 y \times z \times \frac 1 z} + \paren {y \times \frac 1 y \times w \times \frac 1 z}
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | r = \paren {x \times z \times \frac 1 y \times \frac 1 z} + \paren {y \times w \times \frac 1 y \times \frac 1 z}
      | c = {{Real-number-axiom|M2}}
}}
{{eqn | r = \paren {\paren {x \times z} \times \paren {\frac 1 y \times \frac 1 z} } + \paren {\paren {y \times w} \times \paren {\frac 1 y \times \frac 1 z} }
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | r = \paren {\paren {x \times z} + \paren {y \times w} } \times \paren {\frac 1 y \times \frac 1 z}
      | c = {{Real-number-axiom|D}}
}}
{{eqn | r = \paren {\paren {x \times z} + \paren {y \times w} } \times \frac 1 {y z}
      | c = Product of Reciprocals of Real Numbers
}}
{{eqn | r = \frac {\paren {x \times z} + \paren {y \times w} } {y \times z}
      | c = {{Defof|Real Division}}
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of Real Number is Non-Zero

:$\forall x \in \R: x \ne 0 \implies \dfrac 1 x \ne 0$

Proof:
{{AimForCont}} that:
:$\exists x \in \R_{\ne 0}: \dfrac 1 x = 0$
From Real Zero is Zero Element
:$\dfrac 1 x \times x = 0$
But from {{Real-number-axiom|M4}}:
:$\dfrac 1 x \times x = 1$
The result follows by Proof by Contradiction.
{{qed}}
Theorem: Reciprocal of Quotient of Real Numbers

:$\forall x, y \in \R_{\ne 0}: \dfrac 1 {x / y} = \dfrac y x$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {x / y}
      | r = \frac 1 {x \times \dfrac 1 y}
      | c = {{Defof|Real Division}}
}}
{{eqn | r = 1 \times \frac 1 {x \times \dfrac 1 y}
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | r = \paren {y \times \frac 1 y} \times \frac 1 {x \times \dfrac 1 y}
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | r = y \times \paren {\frac 1 y \times \frac 1 {x \times \dfrac 1 y} }
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | r = y \times \frac 1 {y \times \paren {x \times \dfrac 1 y} }
      | c = Product of Reciprocals of Real Numbers
}}
{{eqn | r = y \times \frac 1 {x \times \paren {y \times \dfrac 1 y} }
      | c = {{Real-number-axiom|M2}}
}}
{{eqn | r = y \times \frac 1 {x \times 1}
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | r = y \times \frac 1 x
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | r = \frac y x
      | c = {{Defof|Real Division}}
}}
{{end-eqn}}
{{qed}}
Theorem: Quotient of Quotients of Real Numbers

:$\forall x \in \R, y, w, z \in \R_{\ne 0}: \dfrac {x / y} {w / z} = \dfrac {x \times z} {y \times w}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {x / y} {w / z}
      | r = \frac x y \times \frac 1 {w / z}
      | c = {{Defof|Real Division}}
}}
{{eqn | r = \frac x y \times \frac z w
      | c = Reciprocal of Quotient of Real Numbers
}}
{{eqn | r = \dfrac {x \times z} {y \times w}
      | c = Product of Quotients of Real Numbers
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Real Number with Quotient

:$\forall a, x \in \R, y \in \R_{\ne 0}: \dfrac {a \times x} y = a \times \dfrac x y$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {a \times x} y
      | r = \paren {a \times x} \times \frac 1 y
      | c = {{Defof|Real Division}}
}}
{{eqn | r = a \times \paren {x \times \frac 1 y}
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | r = a \times \frac x y
      | c = {{Defof|Real Division}}
}}
{{end-eqn}}
{{qed}}
Theorem: Neighborhood in Topological Subspace

Let $\struct {X, \tau}$ be a topological space.
Let $S \subseteq X$ be a subset of $X$.
Let $\tau_S$ denote the subspace topology on $S$.
Let $x \in S$ be an arbitrary point of $S$.
Let $E \subseteq S$.
Then:
:$E$ is a neighborhood of $x$ in $\struct {S, \tau_S}$
{{iff}}:
:$\exists D \subseteq X$ such that:
::$D$ is a neighborhood of $x$ in $X$
::$E = D \cap S$.

Proof:
=== Necessary Condition ===
Let $E$ be a neighborhood of $x$ in $\struct {S, \tau_S}$. 
By the definition of neighborhood:
:$\exists U \in \tau_S : x \in U \subseteq E$
Now, by the definition of the subspace topology:
:$\exists V \in \tau: U = V \cap S$
Take $D := V \cup E$.
We have that:
:$V \subseteq D$
and:
:$V \in \tau$
Thus $D$ is a neighborhood of $x$ in $X$.
Therefore it holds true that:
:$D \cap S = \paren {V \cap S} \cup \paren {E \cap S} = U \cup E = E$
{{qed|lemma}}
Theorem: Negative of Quotient of Real Numbers

:$\forall x \in \R, y \in \R_{\ne 0}: \dfrac {-x} y = -\dfrac x y = \dfrac x {-y}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {-x} y
      | r = \frac {\paren {-1} \times x} y
      | c = {{Corollary|Multiplication by Negative Real Number}}
}}
{{eqn | r = \paren {-1} \times \frac x y
      | c = Product of Real Number with Quotient
}}
{{eqn | r = -\frac x y
      | c = {{Corollary|Multiplication by Negative Real Number}}
}}
{{eqn | r = \paren {-1} \times \frac x y
      | c = {{Corollary|Multiplication by Negative Real Number}}
}}
{{eqn | r = \paren {-1} \times 1 \times \frac x y
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | r = \paren {-1} \times \frac {-1} {-1} \times \frac x y
      | c = Real Number Divided by Itself
}}
{{eqn | r = \frac {-1 \times -1} {-1} \times \frac x y
      | c = Product of Real Number with Quotient
}}
{{eqn | r = \frac {-\paren {-1} } {-1} \times \frac x y
      | c = {{Corollary|Multiplication by Negative Real Number}}
}}
{{eqn | r = \frac 1 {-1} \times \frac x y
      | c = Negative of Negative Real Number
}}
{{eqn | r = \frac {1 \times x} {\paren {-1} \times y}
      | c = Product of Quotients of Real Numbers
}}
{{eqn | r = \frac {1 \times x} {-y}
      | c = {{Corollary|Multiplication by Negative Real Number}}
}}
{{eqn | r = \frac x {-y}
      | c = {{Real-number-axiom|M3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Compact Hausdorff Space is Locally Compact

Let $T = \struct {S, \tau}$ be a Hausdorff space which is compact.
Then $T$ is locally compact.

Proof:
By Compact Space is Weakly Locally Compact, $T$ is weakly locally compact.
Thus $T$ is a locally compact Hausdorff space.
{{qed}}
Theorem: Sum of Strictly Positive Real Numbers is Strictly Positive

:$x, y \in \R_{>0} \implies x + y \in \R_{>0}$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = 0
      | c =
}}
{{eqn | lo= \land
      | l = y
      | o = >
      | r = 0
      | c = Real Number Ordering is Compatible with Addition
}}
{{eqn | ll= \leadsto
      | l = x + y
      | o = >
      | r = 0 + 0
      | c = Real Number Inequalities can be Added
}}
{{eqn | r = 0
      | c = {{Real-number-axiom|A3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Real Number is Greater than Zero iff its Negative is Less than Zero

:$\forall x \in \R: x > 0 \iff \paren {-x} < 0$

Proof:
Let $x > 0$.
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-x}
      | o = >
      | r = 0 + \paren {-x}
      | c = {{Real-number-axiom|O2}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = >
      | r = 0 + \paren {-x}
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = >
      | r = \paren {-x}
      | c = {{Real-number-axiom|A3}}
}}
{{end-eqn}}
{{qed|lemma}}
Let $\paren {-x} < 0$.
{{begin-eqn}}
{{eqn | l = \paren {-x}
      | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-x}
      | o = <
      | r = x + 0
      | c = {{Real-number-axiom|O2}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = x + 0
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = x
      | c = {{Real-number-axiom|A3}}
}}
{{end-eqn}}
{{qed}}