avewright/proofwiki-math huggingface dataset:
Theorem: Transitive Relation whose Symmetric Closure is not Transitive

Let $S = \set {p, q}$, where $p$ and $q$ are distinct elements.
Let $\RR = \set {\tuple {p, q} }$.
Then $\RR$ is transitive but its symmetric closure is not.

Proof:
$\RR$ is vacuously transitive because there are no elements $a, b, c \in S$ such that $a \mathrel \RR b$ and $b \mathrel \RR c$.
Let $\RR^\leftrightarrow$ be the symmetric closure of $\RR$.
Then $\RR^\leftrightarrow = \RR \cup \RR^{-1} = \set {\tuple {p, q}, \tuple {q, p} }$.
Then:
:$p \mathrel {\RR^\leftrightarrow} q$ and $q \mathrel {\RR^\leftrightarrow} p$
but:
:$p \not \mathrel {\RR^\leftrightarrow} p$
Therefore $\RR^\leftrightarrow$ is not transitive.
{{qed}}
Category:Transitive Relations
Category:Symmetric Closures
mflhr4zwacm7w7npxhj6e54xft9ht4i
Theorem: Symmetric Closure of Relation Compatible with Operation is Compatible

Let $\struct {S, \circ}$ be a magma.
Let $\RR$ be a relation compatible with $\circ$.
Let $\RR^\leftrightarrow$ denote the symmetric closure of $\RR$.
Then $\RR^\leftrightarrow$ is compatible with $\circ$.

Proof:
By the definition of symmetric closure:
:$\RR^\leftrightarrow = \RR \cup \RR^{-1}$.
Here $\RR^{-1}$ is the inverse of $\RR$.
By Inverse of Relation Compatible with Operation is Compatible, $\RR^{-1}$ is compatible with $\circ$.
Thus by Union of Relations Compatible with Operation is Compatible:
:$\RR^\leftrightarrow = \RR \cup \RR^{-1}$ is compatible with $\circ$.
{{qed}}
Category:Compatible Relations
Category:Symmetric Closures
o980fsks870hx59y0j0x5app9p670ls
Theorem: Singleton is Order-Convex Set

Let $\struct {S, \preceq}$ be an ordered set.
Let $x \in S$.
Then the singleton $\set x$ is order-convex.

Proof:
Let:
:$a, c \in \set x$
:$b \in S$
:$a \preceq b \preceq c$
Then $a = c = x$.
Thus $x \preceq b \preceq x$.
Since $\preceq$ is a ordering, it is antisymmetric.
Thus $b = x$, so $b \in \set x$.
Since this holds for the only such triple, $\set x$ is order-convex.
{{qed}}
Category:Order-Convex Sets
Category:Singletons
cijxfvqxu7y2fw7y2gzkg2zzueqpccp
Theorem: Rule of Transposition/Variant 1/Formulation 2

:$\vdash \paren {p \implies \neg q} \iff \paren {q \implies \neg p}$

Proof:
{{BeginTableau|\vdash \paren {p \implies \neg q} \implies \paren {q \implies \neg p} }}
{{Assumption|1|p \implies \neg q}}
{{Assumption|2|q}}
{{DoubleNegIntro|3|2|\neg \neg q|2}}
{{ModusTollens|4|1, 2|\neg p|1|3}}
{{Implication|5|1|q \implies \neg p|2|4}}
{{Implication|6||\paren {p \implies \neg q} \implies \paren {q \implies \neg p}|1|5}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Transposition/Variant 1/Formulation 2

:$\vdash \paren {p \implies \neg q} \iff \paren {q \implies \neg p}$

Proof:
=== Proof of Forward Implication ===
{{:Rule of Transposition/Variant 1/Formulation 2/Forward Implication/Proof}}
=== Proof of Reverse Implication ===
{{:Rule of Transposition/Variant 1/Formulation 2/Reverse Implication/Proof}}
{{BeginTableau|\vdash \paren {p \implies \neg q} \iff \paren {q \implies \neg p} }}
{{TheoremIntro|1|\paren {p \implies \neg q} \implies \paren {q \implies \neg p}|Rule of Transposition: Forward Implication}}
{{TheoremIntro|2|\paren {q \implies \neg p} \implies \paren {p \implies \neg q}|Rule of Transposition: Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \implies \neg q} \iff \paren {q \implies \neg p}|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Transposition/Variant 1/Formulation 2

:$\vdash \paren {p \implies \neg q} \iff \paren {q \implies \neg p}$

Proof:
{{BeginTableau|\vdash \paren {q \implies \neg p} \implies \paren {p \implies \neg q} }}
{{Assumption|1|q \implies \neg p}}
{{Assumption|2|p}}
{{DoubleNegIntro|3|2|\neg \neg p|2}}
{{ModusTollens|4|1, 2|\neg q|1|3}}
{{Implication|5|1|p \implies \neg q|2|4}}
{{Implication|6||\paren {q \implies \neg p} \implies \paren {p \implies \neg q}|1|5}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Transposition/Variant 1/Formulation 2/Reverse Implication

: $\vdash \left({q \implies \neg p}\right) \implies \left({p \implies \neg q}\right)$

Proof:
{{BeginTableau|\vdash \paren {q \implies \neg p} \implies \paren {p \implies \neg q} }}
{{Assumption|1|q \implies \neg p}}
{{Assumption|2|p}}
{{DoubleNegIntro|3|2|\neg \neg p|2}}
{{ModusTollens|4|1, 2|\neg q|1|3}}
{{Implication|5|1|p \implies \neg q|2|4}}
{{Implication|6||\paren {q \implies \neg p} \implies \paren {p \implies \neg q}|1|5}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Transposition/Variant 1/Formulation 1

:$p \implies \neg q \dashv \vdash q \implies \neg p$

Proof:
{{BeginTableau|p \implies \neg q \vdash q \implies \neg p}}
{{Premise|1|p \implies \neg q}}
{{Assumption|2|q}}
{{DoubleNegIntro|3|2|\neg \neg q|2}}
{{ModusTollens|4|1, 2|\neg p|1|3}}
{{Implication|5|1|q \implies \neg p|2|4}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Transposition/Variant 1/Formulation 1

:$p \implies \neg q \dashv \vdash q \implies \neg p$

Proof:
=== Proof of Forward Implication ===
{{:Rule of Transposition/Variant 1/Formulation 1/Forward Implication/Proof}}
=== Proof of Reverse Implication ===
{{:Rule of Transposition/Variant 1/Formulation 1/Reverse Implication/Proof}}
Theorem: Rule of Transposition/Variant 1/Formulation 1

:$p \implies \neg q \dashv \vdash q \implies \neg p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|cccc||cccc|} \hline
p & \implies & \neg & q & q & \implies & \neg & p \\
\hline
\F & \T & \T & \F & \F & \T & \T & \F \\
\F & \T & \F & \T & \T & \T & \T & \F \\
\T & \F & \T & \F & \F & \F & \F & \T \\
\T & \T & \F & \T & \T & \T & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Transposition/Variant 1/Formulation 1/Forward Implication

:$p \implies \neg q \vdash q \implies \neg p$

Proof:
{{BeginTableau|p \implies \neg q \vdash q \implies \neg p}}
{{Premise|1|p \implies \neg q}}
{{Assumption|2|q}}
{{DoubleNegIntro|3|2|\neg \neg q|2}}
{{ModusTollens|4|1, 2|\neg p|1|3}}
{{Implication|5|1|q \implies \neg p|2|4}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Transposition/Variant 2/Formulation 1

: $\neg p \implies q \dashv \vdash \neg q \implies p$

Proof:
{{BeginTableau|\neg p \implies q \vdash \neg q \implies p}}
{{Premise|1|\neg p \implies q}}
{{Assumption|2|\neg q}}
{{ModusTollens|3|1, 2|\neg \neg p|1|2}}
{{DoubleNegElimination|4|1, 2|p|3}}
{{Implication|5|1|\neg q \implies p|2|4}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Rule of Transposition/Variant 2/Formulation 1

: $\neg p \implies q \dashv \vdash \neg q \implies p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|cccc||cccc|} \hline
\neg & p & \implies & q & \neg & q & \implies & p \\
\hline
\T & \F & \T & \F & \T & \F & \T & \F \\
\T & \F & \T & \T & \F & \T & \T & \F \\
\F & \T & \F & \F & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Transposition/Variant 2/Formulation 1

: $\neg p \implies q \dashv \vdash \neg q \implies p$

Proof:
{{BeginTableau|\neg q \implies p \vdash \neg p \implies q}}
{{Premise|1|\neg q \implies p}}
{{Assumption|2|\neg p}}
{{ModusTollens|3|1, 2|\neg \neg q|1|2}}
{{DoubleNegElimination|4|1, 2|q|3}}
{{Implication|5|1|\neg p \implies q|2|4}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Rule of Transposition/Variant 2/Formulation 1/Forward Implication

:$\neg p \implies q \vdash \neg q \implies p$

Proof:
{{BeginTableau|\neg p \implies q \vdash \neg q \implies p}}
{{Premise|1|\neg p \implies q}}
{{Assumption|2|\neg q}}
{{ModusTollens|3|1, 2|\neg \neg p|1|2}}
{{DoubleNegElimination|4|1, 2|p|3}}
{{Implication|5|1|\neg q \implies p|2|4}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Rule of Transposition/Variant 2/Formulation 1/Forward Implication/Proof

: $\neg p \implies q \vdash \neg q \implies p$

Proof:
{{BeginTableau|\neg p \implies q \vdash \neg q \implies p}}
{{Premise|1|\neg p \implies q}}
{{Assumption|2|\neg q}}
{{ModusTollens|3|1, 2|\neg \neg p|1|2}}
{{DoubleNegElimination|4|1, 2|p|3}}
{{Implication|5|1|\neg q \implies p|2|4}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Rule of Transposition/Variant 2/Formulation 1/Reverse Implication

: $q \implies \neg p \vdash p \implies \neg q$

Proof:
{{BeginTableau|\neg q \implies p \vdash \neg p \implies q}}
{{Premise|1|\neg q \implies p}}
{{Assumption|2|\neg p}}
{{ModusTollens|3|1, 2|\neg \neg q|1|2}}
{{DoubleNegElimination|4|1, 2|q|3}}
{{Implication|5|1|\neg p \implies q|2|4}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Rule of Transposition/Variant 2/Formulation 1/Reverse Implication/Proof

: $\neg q \implies p \vdash \neg p \implies q$

Proof:
{{BeginTableau|\neg q \implies p \vdash \neg p \implies q}}
{{Premise|1|\neg q \implies p}}
{{Assumption|2|\neg p}}
{{ModusTollens|3|1, 2|\neg \neg q|1|2}}
{{DoubleNegElimination|4|1, 2|q|3}}
{{Implication|5|1|\neg p \implies q|2|4}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Rule of Transposition/Variant 2/Formulation 2/Forward Implication

:$\vdash \paren {\neg p \implies q} \implies \paren {\neg q \implies p}$

Proof:
{{BeginTableau|\vdash \paren {\neg p \implies q} \implies \paren {\neg q \implies p} }}
{{Assumption|1|\neg p \implies q}}
{{Assumption|2|\neg q}}
{{ModusTollens|3|1, 2|\neg \neg p|1|2}}
{{DoubleNegElimination|4|1, 2|p|3}}
{{Implication|5|1|\neg q \implies p|2|4}}
{{Implication|6||\paren {\neg p \implies q} \implies \paren {\neg q \implies p}|1|5}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|4}}
Theorem: Rule of Transposition/Variant 2/Formulation 2/Reverse Implication

:$\vdash \paren {\neg q \implies p} \implies \paren {\neg p \implies q}$

Proof:
{{BeginTableau|\vdash \paren {\neg q \implies p} \implies \paren {\neg p \implies q} }}
{{Assumption|1|\neg q \implies p}}
{{Assumption|2|\neg p}}
{{ModusTollens|3|1, 2|\neg \neg q|1|2}}
{{DoubleNegElimination|4|1, 2|q|3}}
{{Implication|5|1|\neg p \implies q|2|4}}
{{Implication|6||\paren {\neg q \implies p} \implies \paren {\neg p \implies q}|1|5}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|4}}
Theorem: Rule of Transposition/Variant 2/Formulation 2

:$\vdash \paren {\neg p \implies q}\ \iff \paren {\neg q \implies p}$

Proof:
{{BeginTableau|\vdash \paren {\neg p \implies q} \implies \paren {\neg q \implies p} }}
{{Assumption|1|\neg p \implies q}}
{{Assumption|2|\neg q}}
{{ModusTollens|3|1, 2|\neg \neg p|1|2}}
{{DoubleNegElimination|4|1, 2|p|3}}
{{Implication|5|1|\neg q \implies p|2|4}}
{{Implication|6||\paren {\neg p \implies q} \implies \paren {\neg q \implies p}|1|5}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|4}}
Theorem: Rule of Transposition/Variant 2/Formulation 2

:$\vdash \paren {\neg p \implies q}\ \iff \paren {\neg q \implies p}$

Proof:
{{BeginTableau|\vdash \paren {\neg p \implies q} \iff \paren {\neg q \implies p} }}
{{TheoremIntro|1|\paren {\neg p \implies q} \implies \paren {\neg q \implies p}|Rule of Transposition: Forward Implication}}
{{TheoremIntro|2|\paren {\neg q \implies p} \implies \paren {\neg p \implies q}|Rule of Transposition: Reverse Implication}}
{{BiconditionalIntro|3||\paren {\neg p \implies q} \iff \paren {\neg q \implies p}|1|2}}
{{EndTableau|qed}}
{{LEM||4}}
Theorem: Rule of Transposition/Variant 2/Formulation 2

:$\vdash \paren {\neg p \implies q}\ \iff \paren {\neg q \implies p}$

Proof:
{{BeginTableau|\vdash \paren {\neg q \implies p} \implies \paren {\neg p \implies q} }}
{{Assumption|1|\neg q \implies p}}
{{Assumption|2|\neg p}}
{{ModusTollens|3|1, 2|\neg \neg q|1|2}}
{{DoubleNegElimination|4|1, 2|q|3}}
{{Implication|5|1|\neg p \implies q|2|4}}
{{Implication|6||\paren {\neg q \implies p} \implies \paren {\neg p \implies q}|1|5}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|4}}
Theorem: Boundary of Polygon is Topological Boundary

Let $P$ be a polygon embedded in $\R^2$.
Denote the boundary of $P$ as $\partial P$.
Let $\Int P$ and $\Ext P$ denote the interior and exterior of $\partial P$, where $\partial P$ is considered as a Jordan curve.
Then the topological boundary of $\Int P$ is equal to $\partial P$, and the topological boundary of $\Ext P$ is equal to $\partial P$.

Proof:
Denote the topological boundary of $\Int P$ as $\partial \Int P$, and denote the topological boundary of $\Ext P$ as $\partial \Ext P$.
Theorem: Convex Component of Open Set in GO-Space is Open

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space.
Let $A$ be a $\tau$-open subset of $S$.
Let $C$ be a convex component of $A$ in $S$
Then $C$ is open relative to $\tau$.

Proof:
Note: the term '''convex''' will be used here to refer to a set that is order-convex in $S$.
Since $\struct {S, \preceq, \tau}$ is a generalized ordered space, $\tau$ has a basis $\BB$ consisting of open convex sets.
Let $x \in C$.
Then $x \in A$, and $A$ is open in $S$.
Thus by the definition of a basis, there is a $U \in \BB$ such that $x \subseteq U \subseteq A$.
Since $U$ is convex and contains $x$, $U \subseteq C$.
Thus $C$ contains an open neighborhood of each of its points, so $C$ is open.
{{qed}}
Category:Generalized Ordered Spaces
Category:Total Orderings
59w6v8zkchr2125l3uvj3c60nol54j3
Theorem: Jordan Curve and Jordan Arc form Two Jordan Curves

Let $\gamma: \closedint a b \to \R^2$ be a Jordan curve, where $\closedint a b$ is the closed real interval between $a, b \in \R$ with $a < b$.
Let the interior of $\gamma$ be denoted $\Int \gamma$.
Let the image of $\gamma$ be denoted $\Img \gamma$.
Let $\sigma: \closedint c d \to \R^2$ be a Jordan arc such that:
:$\map \sigma c, \map \sigma d \in \Img \gamma$
and:
:$\forall t \in \openint c d: \map \sigma t \in \Int \gamma$
Let $t_1 = \map {\gamma^{-1} } {\map \sigma c}$.
Let $t_2 = \map {\gamma^{-1} } {\map \sigma d}$.
Let $t_1 < t_2$.
Define:
:$-\sigma: \closedint c d \to \Img \sigma$ by $-\map \sigma t = \map \sigma {c + d - t}$
Let $*$ denote concatenation of paths.
Let $\gamma \restriction_{\closedint a {t_1} }$ denote the restriction of $\gamma$ to $\closedint a {t_1}$.
Define:
:$\gamma_1 = \gamma \restriction_{\closedint a {t_1} } * \sigma * \gamma {\restriction_{\closedint {t_2} b} }$
Define:
:$\gamma_2 = \gamma \restriction_{\closedint {t_1} {t_2} } * \paren {-\sigma}$
Then $\gamma_1$ and $\gamma_2$ are Jordan curves such that:
:$\Int {\gamma_1} \cup \Int {\gamma_2} \cup \paren {\Img \sigma \setminus \set {\map \sigma c , \map \sigma d } } = \Int \gamma$

Proof:
=== $\gamma_1$ and $\gamma_2$ are Jordan curves ===
Let $\closedint {a_1}{b_1}$ denote the domain of $\gamma_1$, and $\closedint {a_2}{b_2}$ denote the domain of $\gamma_2$.
As:
:$\Int \gamma$ and $\Img \gamma$ are disjoint by the Jordan Curve Theorem
and:
:$\map \sigma {\openint c d} \subseteq \Int \gamma$
it follows that:
:$\Img \gamma \cap \Img \sigma = \set {\map \sigma c, \map \sigma d}$.
As $\gamma$ is a Jordan curve, it follows that $\gamma {\restriction_{\closedint a {t_1} } }$ and $\gamma {\restriction_{\closedint {t_2} b} }$ intersect only in $\map \gamma a$.
It follows that:
:$\map {\gamma_1 }{t_1} \ne \map {\gamma_1} {t_2}$ for all $t_1 ,t_2 \in \hointr {a_1} {b_1}$ with $t_1 \ne t_2$
As the initial point of $\gamma_1$ is $\map \gamma a$, and the final point of $\gamma_1$ is $\map \gamma b = \map \gamma a$, it follows that $\gamma_1$ is a Jordan curve.
As $\Img {-\sigma} = \Img \sigma$, it follows that:
:$\map {\gamma_2 }{t_1} \ne \map {\gamma_2 }{t_2}$ for all $t_1 ,t_2 \in \hointr {a_2}{b_2}$ with $t_1 \ne t_2$
As $\map \gamma {t_1} = \map \sigma c = -\map \sigma d$, it follows that $\gamma_2$ is a Jordan curve.
{{qed|lemma}}
Theorem: Restriction of Total Ordering is Total Ordering

Let $\struct {S, \preceq}$ be a total ordering.
Let $T \subseteq S$.
Let $\preceq \restriction_T$ be the restriction of $\preceq$ to $T$.
Then $\preceq \restriction_T$ is a total ordering of $T$.

Proof:
By Restriction of Ordering is Ordering, $\preceq \restriction_T$ is an ordering.
Let $x, y \in T$.
As $T \subseteq S$ it follows by definition of subset that:
:$x, y \in S$
As $\preceq$ is a total ordering:
:$\tuple {x, y} \in {\preceq}$
or:
:$\tuple {y, x} \in {\preceq}$
Suppose $\tuple {x, y} \in {\preceq}$.
As $x, y \in T$, it follows by definition of cartesian product that:
:$\tuple {x, y} \in T \times T$
Thus:
:$\tuple {x, y} \in \paren {T \times T} \cap {\preceq}$
By definition of the restriction of $\preceq$ to $T$:
:$\paren {T \times T} \cap {\preceq} = {\preceq \restriction_T}$
That is:
:$\tuple {x, y} \in {\preceq \restriction_T}$
A similar argument shows that:
:$\tuple {y, x} \in {\preceq} \implies \tuple {y, x} \in {\preceq \restriction_T}$
Thus $\preceq \restriction_T$ is a total ordering of $T$.
{{qed}}
Theorem: Ordering Cycle implies Equality/General Case

Let $\struct {S,\preceq}$ be an ordered set.
Let $x_0, x_1, \dots, x_n \in S$.
Suppose that for $k = 0, 1, \dots, n - 1: x_k \preceq x_{k + 1}$.
Suppose also that $x_n \preceq x_0$.
Then $x_0 = x_1 = \dots = x_n$.

Proof:
Since $\preceq$ is an ordering it is transitive and antisymmetric.
By Transitive Chaining, it follows from the first premise that for all $k$ with $0 \le k \le n$:
:$x_0 \preceq x_k$
and also:
:$x_k \preceq x_n$
The other premise states that $x_n \preceq x_0$.
By transitivity of $\preceq$, this combines with the above to:
:$x_k \preceq x_0$
Since $\preceq$ is antisymmetric, this means that $x_0 = x_k$ for $0 \le k \le n$.
That is, $x_0 = x_1 = \dots = x_n$.
{{qed}}
Theorem: Finite Non-Empty Subset of Ordered Set has Maximal and Minimal Elements

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ be a finite, non-empty subset of $S$.
Then $T$ has a maximal element and a minimal element.

Proof:
We will show that each finite subset of $S$ has a minimal element.
The existence of a maximal element then follows from duality.
Proof by induction:
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:Every set with $n$ elements has a minimal element.
Theorem: Star Convex Set is Path-Connected

Let $A$ be a star convex subset of a topological vector space $V$ over $\R$ or $\C$.
Then $A$ is path-connected.

Proof:
Let $x_1, x_2 \in A$.
Let $a \in A$ be a star center of $A$.
By definition of star convex set:
:$\forall t \in \closedint 0 1: x_1 + \paren {1 - t} a, t x_2 + \paren {1 - t} a \in A$
Define two paths $\gamma_1, \gamma_2: t \in \closedint 0 1 \to A$ by:
:$\map {\gamma_1} t =  t x_1 + \paren {1 - t} a$
:$\map {\gamma_2} t = t a + \paren {1 - t} x_2$
By definition of topological vector space, it follows that $\gamma_1$ and $\gamma_2$ are continuous.
Because:
:$\map {\gamma_2} t = \paren {1 - t} x_2 + \paren {1 - \paren {1 - t} } a$
and:
:$\paren {1 - t} \in \closedint 0 1$
it follows that:
:$\map {\gamma_2} t \in A$
Note that:
:$\map {\gamma_1} 0 = x_1$, $\map {\gamma_1} 1 = \map {\gamma_2} 0 = a$
and:
:$\map {\gamma_2} 1 = x_2$
Define $\gamma: \closedint 0 1 \to A$ as the concatenation $\gamma_1 * \gamma_2$.
Then $\gamma$ is a path in $A$ joining $x_1$ and $x_2$.
It follows by definition that $A$ is path-connected.
{{qed}}
Theorem: Minimal Element of Chain is Smallest Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $C$ be a chain in $S$.
Let $m$ be a minimal element of $C$.
Then $m$ is the smallest element of $C$.

Proof:
Let $x \in C$.
Since $m$ is minimal in $C$, $x \nprec m$.
Since $C$ is a chain, $x = m$ or $m \prec x$.
Thus for each $x \in C$, $m \preceq x$.
Therefore $m$ is the smallest element of $C$.
{{qed}}
Theorem: Maximal Element of Chain is Greatest Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $C$ be a chain in $S$.
Let $m$ be a maximal element of $C$.
Then $m$ is the greatest element of $C$.

Proof:
Let $x \in C$.
Since $m$ is maximal in $C$, $m \nprec x$.
Since $C$ is a chain, $x = m$ or $x \prec m$.
Thus for each $x \in C$, $x \preceq m$.
Therefore $m$ is the greatest element of $C$.
{{qed}}
Theorem: Modus Ponendo Ponens/Variant 3

:$\vdash \paren {\paren {p \implies q} \land p} \implies q$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies q} \land p} \implies q}}
{{Assumption|1|\paren {p \implies q} \land p}}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|p|1|2}}
{{ModusPonens|4|1|q|2|3}}
{{Implication|5||\paren {\paren {p \implies q} \land p} \implies q|1|4}}
{{EndTableau}}
{{Qed}}
Theorem: Modus Ponendo Ponens/Variant 3

:$\vdash \paren {\paren {p \implies q} \land p} \implies q$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|c|} \hline
((p & \implies & q) & \land & p) & \implies & q \\
\hline
\F & \T & \F & \F & \F & \T & \F \\
\F & \T & \T & \F & \F & \T & \T \\
\T & \F & \F & \F & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Material Equivalence/Formulation 1/Proof 1

:$p \iff q \dashv \vdash \paren {p \implies q} \land \paren {q \implies p}$

Proof:
{{BeginTableau|p \iff q \vdash \paren {p \implies q} \land \paren {q \implies p} }}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{BiconditionalElimination|3|1|q \implies p|1|2}}
{{Conjunction|4|1|\paren {p \implies q} \land \paren {q \implies p}|2|3}}
{{EndTableau}}
{{BeginTableau|\paren {p \implies q} \land \paren {q \implies p} \vdash p \iff q}}
{{Premise|1|\paren {p \implies q} \land \paren {q \implies p} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|q \implies p|1|2}}
{{BiconditionalIntro|4|1|p \iff q|2|3}}
{{EndTableau}}
{{qed}}
Theorem: Order-Convex Set Characterization

Let $\struct {S, \preceq, \tau}$ be an ordered set.
Let $C \subseteq S$.
{{TFAE}}
{{begin-axiom}}
{{axiom | n = 1
        | t = $C$ is order-convex.
}}
{{axiom | n = 2
        | t = $C$ is the intersection of an upper section with a lower section.
}}
{{axiom | n = 3
        | t = $C$ is the intersection of its upper closure with its lower closure.
}}
{{end-axiom}}

Proof:
=== $(2)$ implies $(1)$ ===
Follows from Upper Section is Order-Convex, Lower Section is Order-Convex, and Intersection of Order-Convex Sets is Order-Convex.
{{qed|lemma}}
Theorem: Upper Closure is Upper Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a subset of $S$.
Let $U$ be the upper closure of $T$.
Then $U$ is an upper section.

Proof:
Let $a \in U$.
Let $b \in S$ with $a \preceq b$.
By the definition of upper closure, there is a $t \in T$ such that $t \preceq a$.
By transitivity, $t \preceq b$.
Thus, again by the definition of upper closure:
:$b \in U$
Since this holds for all such $a$ and $b$, $U$ is an upper section.
{{qed}}
Theorem: Open Ray is Open in GO-Space/Definition 1

Let $\struct {S, \preceq, \tau}$ be a generalized ordered space.
Let $p \in S$.
Then:
:$p^\prec$ and $p^\succ$ are $\tau$-open
where:
:$p^\prec$ is the strict lower closure of $p$
:$p^\succ$ is the strict upper closure of $p$.

Proof:
We will prove that $U = p^\succ$ is $\tau$-open.
That $p^\prec$ is $\tau$-open will follow by duality.
Let $u \in U$.
Since $p \notin U$, $p \ne u$.
By definition of GO-space, $\tau$ is Hausdorff.
From $T_2$ Space is $T_1$ Space, $\tau$ is $T_1$.
Thus by definition of GO-space, there is an open, order-convex set $M$ such that $u \in M$ and $p \notin M$.
Next we will show that $M \subseteq U$:
Let $x \in S \setminus U$.
Then $x \preceq p \preceq u$.
{{AimForCont}} $x \in M$.
Since $x, u \in M$, $p \in M$ because $M$ is order-convex, contradicting the choice of $M$.
Thus $x \notin M$.
Since this hold for all $x \in S \setminus U$, $M \subseteq U$.
Thus $U$ contains a neighborhood of each of its points.
From Set is Open iff Neighborhood of all its Points, $U$ is open.
{{qed}}