avewright/proofwiki-math huggingface dataset:
Theorem: Jordan Curve Bounding Loop in Euclidean Plane

Let $f : \closedint 0 1 \to \R^2$ be a loop in the Euclidean plane $\R^2$.
Let $\epsilon \in \R_{>0}$.
Then there exists a Jordan curve $\gamma : \closedint 0 1 \to \R^2$ such that $\Img f \subseteq \Int \gamma$, and for all $t \in \closedint 0 1$:
:$\map d {\map \gamma t, \Img f} < \epsilon$
where $\map d {\map \gamma t, \Img f}$ denotes the Euclidean distance between $\map \gamma t$ and $\Img f$.
Here $\Img f$ denotes the image of $f$, and $\Int \gamma$ denotes the interior of $\gamma$.

Proof:
=== Cast a ray from an extreme point of $\Img f$===
Let $\norm {\map f t}: \closedint 0 1 \to \R$ denote the Euclidean norm of $\map f t$, considered as a function of $t$.
From Norm on Vector Space is Continuous Function and Composite of Continuous Mappings between Metric Spaces is Continuous, it follows that $\norm {\map f t}$ is continuous.
From Closed Real Interval is Compact Space, it follows that $\closedint 0 1$ is compact.
Set $\ds K := \max_{t \mathop \in \closedint 0 1} \norm {\map f t}$.
From the Extreme Value Theorem it follows that $K$ is well-defined, and there exists $t_0 \in \closedint 0 1$ such that:
:$\ds \norm {\map f {t_0} } = K$
By definition of closed ball, it follows that:
:$\Img f \subseteq \map {B_K^-} \bszero$
where $\map {B_K^-} \bszero$ denotes a closed ball with center equal to the origin of $\R^2$.
Let $\LL : \hointr 0 \infty \to \R^2$ be a ray with start point $\map f {t_0}$ defined by:
:$\map \LL r = r \map f {t_0} + \map f {t_0}$
Using {{NormAxiomVector|2}}, it follows that for all $r \in \openint 0 \infty$:
:$\norm {\map \LL r} = \paren {1 + r} \norm {\map f {t_0} } > K$
which shows that $\map \LL r \notin \Img f$.
Also, the equality shows that $\norm {\map \LL r}$ is strictly increasing.
Theorem: Interior of Jordan Curve is Simply Connected

Let $\gamma : \closedint 0 1 \to \R^2$ be a Jordan curve.
Let $\Int \gamma$ denote the interior of $\gamma$.
Let $\tau_0$ denote the subspace topology on $\Int \gamma$, induced by the Euclidean topology on $\R^2$.
Then $\struct {\Int \gamma, \tau_0}$ is simply connected.

Proof:
Let $\map {B_1} { \mathbf 0 }$ denote the open ball in $\R^2$ with radius $1$ and center equal to the origin $\bszero$.
We are given $\Int \gamma$ is the interior of $\gamma$.
From the Jordan-Schönflies Theorem, it follows that $\Int \gamma$ and $\map {B_1} { \mathbf 0 }$ are homeomorphic.
From Open Ball is Simply Connected, it follows that $\map {B_1} { \mathbf 0 }$, considered as a subspace of $\R^2$, is simply connected.
From Simple Connectedness is Preserved under Homeomorphism, it follows that $\struct {\Int \gamma, \tau_0}$ is simply connected.
{{qed}}
Category:Jordan Curves
Category:Simply Connected Spaces
jknxbxny8lnya7ribc13awnuebvccmq
Theorem: Equivalence of Definitions of Matroid Circuit Axioms/Lemma 2

Let $X \subseteq S$ and $y \in S \setminus X$.
Then:
:$\map \rho {X \cup \set y} = \map \rho X$ {{iff}} $\exists C \in \mathscr C : y \in C \subseteq X \cup \set y$

Proof:
Let $X = \set{x_1, \ldots, x_q}$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho {X \cup \set y}
      | r = \map t {x_1, \ldots, x_q, y}
      | c = Definition of $\rho$
}}
{{eqn | r = \map t {x_1, \ldots, x_q} + \map \theta {x_1, \ldots, x_q, y}_{q+1}
      | c = Definition of $t$
}}
{{eqn | r = \map \rho X + \map \theta {x_1, \ldots, x_q, y}_{q+1}
      | c = Definition of $t$
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \map \rho {X \cup \set y} = \map \rho X
      | o = \leadstoandfrom
      | r = \map \theta {x_1, \ldots, x_q, y}_{q+1} = 0
}}
{{eqn | o = \leadstoandfrom
      | r = \exists C \in \mathscr C : y \in C \subseteq X \cup \set y
      | c = Definition of $\theta$
}}
{{end-eqn}}
{{qed}}
Category:Equivalence of Definitions of Matroid Circuit Axioms
cm1dtdrhbj2djkt565b0dt3ewpdct74
Theorem: Cartesian Product of Intervals is Convex Set

Let $n \in \N$.
For all $k \in \set {1, \ldots, n}$, let $\Bbb I_k$ be a real interval of any of the real interval types.
Then the cartesian product $\Bbb I_1 \times \ldots \times \Bbb I_n$ is a convex set.

Proof:
Let $\mathbf x, \mathbf y \in \Bbb I_1 \times \ldots \times \Bbb I_n$ with:
{{begin-eqn}}
{{eqn | l = \mathbf x
      | r = \tuple {x_1, \ldots, x_n}
}}
{{eqn | l = \mathbf y
      | r = \tuple {y_1, \ldots, y_n}
}}
{{end-eqn}}
where $x_k , y_k \in \Bbb I_k$ for all $k \in \set {1, \ldots, n}$.
Let $t \in \closedint 0 1$.
Suppose that $x_k \le y_k$.
It follows that:
{{begin-eqn}}
{{eqn | l = x_k
      | r = t x_k + \paren {1-t} x_k
}}
{{eqn | o = \le
      | r = t x_k + \paren {1-t} y_k
      | c = as $1-t \in \closedint 0 1$
}}
{{eqn | o = \le
      | r = t y_k + \paren {1-t} y_k
}}
{{eqn | r = y_k
}}
{{end-eqn}}
By definition of real interval, it follows that $t x_k + \paren {1-t} y_k \in \Bbb I_k$.
If instead $x_k \ge y_k$, it follows by similar calculations that:
:$x_k \ge t x_k + \paren {1-t} y_k \ge y_k$
By definition of real interval, it follows that $t x_k + \paren {1-t} y_k \in \Bbb I_k$.
It follows that $t \mathbf x + \paren {1-t} \mathbf y \in \Bbb I_1 \times \ldots \times \Bbb I_n$.
By definition of convex set, it follows that $\Bbb I_1 \times \ldots \times \Bbb I_n$ is a convex set.
{{qed}}
Category:Convex Sets (Vector Spaces)
bvm0c8q26r7diurp21hj5td5h3wt42y
Theorem: Cartesian Product of Intervals is Simply Connected

Let $n \in \N$.
For all $k \in \set {1, \ldots, n}$, let $\Bbb I_k$ be a real interval of any of the real interval types.
Let $\tau_0$ denote the subspace topology on the cartesian product $\Bbb I_1 \times \ldots \times \Bbb I_n$, induced by the Euclidean topology on $\R^n$.
Then $\struct {\Bbb I_1 \times \ldots \times \Bbb I_n, \tau_0}$ is simply connected.

Proof:
The result follows from Cartesian Product of Intervals is Convex Set and Convex Set is Simply Connected.
{{qed}}
Category:Simply Connected Spaces
8z7eo0mw9kif2mdpq53zqxjrnfruwck
Theorem: Characterization of Ergodicity in terms of Koopman Operator

Let $\struct {X, \BB, \mu}$ be a probability space.
Let $T: X \to X$ be a measure-preserving transformation.
Let $\map \MM {X, \R}$ be the set of $\BB$-measurable functions.
Let $\map {\LL^2} \mu$ denote the Lebesgue $2$-space.
Let $U_T : \map \MM {X, \R} \to \map \MM {X, \R}$ be the Koopman operator:
:$U_T: f \mapsto f \circ T$
{{refactor|level = medium|several statements rolled into one which should be separated out into their own pages}}
{{tidy|I'll get round to it in due course}}
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$T$ is ergodic}}
{{item|(2):|For all $f \in \map \MM {X, \R}$:
:if $\map {U_T} f {{=}} f$, then $f$ is constant $\mu$-a.e.
}}
{{item|(3):|For all $f \in \map \MM {X, \R}$:
:if $\map {U_T} f {{=}} f$ for $\mu$-a.e., then $f$ is constant $\mu$-a.e.
}}
{{item|(4):|For all $f \in \map {\LL ^2} \mu$:
:if $\map {U_T} f {{=}} f$, then $f$ is constant $\mu$-a.e.
}}
{{item|(5):|For all $f \in \map {\LL ^2} \mu$:
:if $\map {U_T} f {{=}} f$ for $\mu$-a.e., then $f$ is constant $\mu$-a.e.
}}
{{end-itemize}}

Proof:
=== $(1) \implies (3)$ ===
This is clear, since $(3)$ is exactly the definition of ergodicity.
{{qed|lemma}}
Theorem: Uniform Prisms are Countably Infinite

There are countably infinite different varieties of uniform prisms.

Proof:
{{Recall|Uniform Prism}}
{{:Definition:Uniform Prism}}
Hence a uniform prism is made of:
:$2$ bases which are regular polygons
:as many lateral faces as there are sides of one of the bases.
Hence for each type of regular polygon there exists a corresponding uniform prism.
There exists a type of regular polygon for each natural number greater than or equal to $3$.
There exists countably infinite set of natural numbers greater than or equal to $3$.
Hence the result.
{{qed}}
Category:Uniform Prisms
Category:Countably Infinite Sets
5iq5xfnmurvnvlz3fislcm3jdnj61xe
Theorem: Connected Graph is Tree iff Removal of One Edge makes it Disconnected

Let $G = \struct {V, E}$ be a connected simple graph.
Then $G$ is a tree {{iff}}:
:for all edges $e$ of $G$, the edge deletion $G \setminus \set e$ is disconnected.

Proof:
=== Sufficient Condition ===
{{:Connected Graph is Tree iff Removal of One Edge makes it Disconnected/Sufficient Condition/Proof 1}}{{qed|lemma}}
Theorem: Connected Graph is Tree iff Removal of One Edge makes it Disconnected

Let $G = \struct {V, E}$ be a connected simple graph.
Then $G$ is a tree {{iff}}:
:for all edges $e$ of $G$, the edge deletion $G \setminus \set e$ is disconnected.

Proof:
Let $G$ be a tree.
Then by definition $G$ has no circuits.
From Condition for Edge to be Bridge, every edge of $G$ is a bridge.
Thus by definition of bridge, removing any edge of $G$ will disconnect $G$.
Theorem: Connected Graph is Tree iff Removal of One Edge makes it Disconnected

Let $G = \struct {V, E}$ be a connected simple graph.
Then $G$ is a tree {{iff}}:
:for all edges $e$ of $G$, the edge deletion $G \setminus \set e$ is disconnected.

Proof:
Let $G$ be a tree.
Hence {{afortiori}} $G$ has no cycles.
Let $v, v' \in V$.
Let the edge $\set {v, v'}$ be removed.
{{AimForCont}} $G$ is still connected.
Then {{apriori}} $v$ and $v'$ are connected.
By If Vertices are Connected then Path Exists between them, there is a path $\tuple {v, v_1, \ldots, v'}$ of length $2$ or more.
Hence $\tuple {v, v_1, \ldots, v', v}$ is a cycle in $G$.
This contradicts the statement that $G$ has no cycles.
The result follows by Proof by Contradiction.
Theorem: Reverse Triangle Inequality/Seminormed Vector Space

Let $\struct {K, +, \circ}$ be a division ring with norm $\norm {\,\cdot\,}_K$.
Let $X$ be a vector space over $K$.
Let $p$ be a seminorm on $X$.
Then:
:$\forall x, y \in X : \size {\map p x - \map p y} \le \map p {x - y}$
{{explain|$\size {\map p x - \map p y}$}}

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map p x - \map p y
      | r = \map p {x - y + y} - \map p y
}}
{{eqn | o = \le
      | r = \map p {x - y} + \map p y - \map p y
      | c = {{SeminormAxiom|3}}
}}
{{eqn | r = \map p {x - y}
}}
{{end-eqn}}
We also have:
{{begin-eqn}}
{{eqn | l = \map p y - \map p x
      | r = \map p {y - x + x} - \map p x
}}
{{eqn | o = \le
      | r = \map p {y - x} + \map p x - \map p x
      | c = {{SeminormAxiom|3}}
}}
{{eqn | r = \map p {y - x}
}}
{{eqn | r = \norm {-1}_K \map p {x - y}
      | c = {{SeminormAxiom|2}}
}}
{{eqn | r = \map p {x - y}
      | c = Norm of Negative of Unity of Division Ring
}}
{{end-eqn}}
Therefore:
:$-\map p {x - y} \le \map p x - \map p y \le \map p {x - y}$
{{explain|There is a step missing: $-\map p {x - y} \le \map p x - \map p y$ not explicitly demonstrated}}
In view of {{Defof|Absolute Value}}, the claim is proved.
{{qed}}
Category:Triangle Inequality
Category:Seminorms
bqn0o2hpswxksqxa66akpczxl4a56uc
Theorem: Connected Graph is Tree iff Removal of One Edge makes it Disconnected/Necessary Condition

Let $G = \struct {V, E}$ be a connected simple graph such that:
:for all edges $e$ of $G$, the edge deletion $G \setminus \set e$ is disconnected.
Then $G$ is a tree.

Proof:
Let $G$ be a connected simple graph such that for all edges $e$ of $G$, the edge deletion $G \setminus \set e$ is disconnected.
Hence, by definition, every edge of $G$ must be a bridge.
So by Condition for Edge to be Bridge, $G$ has no circuits.
Hence $G$ is a tree by definition.
Theorem: Finite Connected Simple Graph is Tree iff Size is One Less than Order/Lemma

:$G$ has at least one leaf node.

Proof:
Let $G = \struct {V, E}$ be a non-edgeless connected finite simple graph.
Let us select $v_1 \in V$ and some $v_2 \in V$ which is adjacent to $v_1$.
Such will always exist because $G$ is connected and not edgeless.
For $k \ge 2$, either $v_k$ is adjacent to $v_{k - 1}$ and no other, or it is adjacent to $v_{k - 1}$ and some $v_{k + 1}$ where $v_{k + 1} \ne v_{k - 1}$.
Since there are no cycles in $G$, each of $v_1, v_2, \ldots, v_{k + 1}$ are all distinct.
Hence as $G$ is finite, the process will terminate.
Thus $v_{k + 1}$ will be a leaf node.
{{qed}}
Theorem: Sequence of Natural Powers of Right Shift Operator in 2-Sequence Space Converges in Weak Operator Topology

Let $\struct {\ell^2, \norm {\, \cdot \,}_2}$ be the $2$-sequence normed vector space.
Let $\map {CL} {\ell^2} := \map {CL} {\ell^2, \ell^2}$ be the continuous linear transformation space.
Let $R \in \map {CL} {\ell^2}$ be the right shift operator over $\ell^2$.
Let $\sequence {R^n}_{n \mathop \in \N}$ be a sequence.
Let $\mathbf 0 \in \map {CL} {\ell^2}$ be the zero mapping.
Then $\sequence {R^n}_{n \mathop \in \N}$ converges to $\mathbf 0$ in the weak operator topology.

Proof:
By Representation Theorem:
:$\ds \forall \phi \in \map {CL} {\ell^2, \C} : \exists \mathbf x_\phi = \sequence {\map {\mathbf x_\phi} k}_{k \mathop \in \N} \in \ell^2 : \forall \mathbf a = \sequence {\map {\mathbf a} k}_{k \mathop \in \N} \in \ell^2 : \map \phi {\mathbf a} = \sum_{k \mathop = 1}^\infty \map {\mathbf a} k \paren{\map {\mathbf x_\phi} k}^*$
where $*$ denotes the complex conjugation.
Furthermore:
{{begin-eqn}}
{{eqn | q = \forall \mathbf a \in \ell^2 : \forall \phi \in \map {CL} {\ell^2, \C}
      | l = \size {\map \phi {R^n \mathbf a} }^2
      | r = \size {\sum_{k \mathop = 1}^\infty \map {\mathbf a} k \paren{\map {\mathbf x_\phi} {n + k} }^* }^2
}}
{{eqn | o = \le
      | r = \norm {\mathbf a}^2_2 \sum_{k \mathop = 1}^\infty \size {\map {\mathbf x_\phi} {n + k} }^2
      | c = Cauchy-Schwarz Inequality
}}
{{eqn | ll = \leadsto
      | l = \lim_{n \mathop \to \infty } \size {\map \phi {R^n \mathbf a} }^2
      | o = \le
      | r = \lim_{n \mathop \to \infty} \norm {\mathbf a}^2_2 \sum_{k \mathop = 1}^\infty \size {\map {\mathbf x_\phi} {n + k} }^2
}}
{{eqn | r = \norm {\mathbf a}^2_2 \lim_{n \mathop \to \infty} \sum_{k \mathop = 1}^\infty \size {\map {\mathbf x_\phi} {n + k} }^2
      | c = Multiple Rule for Real Sequences
}}
{{eqn | r = \norm {\mathbf a}^2_2 \sum_{k \mathop = 1}^\infty  \lim_{n \mathop \to \infty} \size {\map {\mathbf x_\phi} {n + k} }^2
      | c = Exchange of Limits
}}
{{eqn | r = 0
      | c = {{Defof|P-Sequence Space}}, Terms in Convergent Series Converge to Zero
}}
{{end-eqn}}
Hence, $\sequence {R^n}_{n \mathop \in \N}$ converges to $\mathbf 0 \in \map {CL} {\ell^2}$ in the weak operator topology.
{{qed}}
Theorem: Desargues' Theorem/Converse

Let $\triangle ABC$ and $\triangle A'B'C'$ be triangles lying in the same or different planes.
Let:
:$BC$ meet $B'C'$ in $L$
:$CA$ meet $C'A'$ in $M$
:$AB$ meet $A'B'$ in $N$
where $L, M, N$ are collinear.
Then the lines $AA'$, $BB'$ and $CC'$ intersect in the point $O$.

Proof:
:500px
Let $L$, $M$ and $N$ be collinear {{hypothesis}}.
Then $\triangle BB'N$ and $\triangle CC'M$ are perspective with center $L$ ($L = BC \cap B'C' \cap MN$)
From Desargues' Theorem:
:$O = BB' \cap CC'$
:$A = BN \cap CM$
:$A' = C'M \cap B'N$
are collinear.
Thus:
:$AA' \cap BB' \cap CC' = O$
Hence $\triangle ABC$ and $\triangle A'B'C'$ are perspective with center $O$.
{{explain|Define what is meant by "perspective".}}
{{qed}}
Theorem: Circuits of Matroid iff Matroid Circuit Axioms

Let $S$ be a finite set.
Let $\mathscr C$ be a non-empty set of subsets of $S$.
Then:
:$\mathscr C$ is the set of circuits of a matroid on $S$
{{iff}}
:$\mathscr C$ satisfies the circuit axioms

Proof:
From Equivalence of Definitions of Matroid Circuit Axioms it is sufficient to show:
:$(\text a)\quad$if $\mathscr C$ is the set of circuits of a matroid then $\mathscr C$ satisfies circuit axioms (formulation 1)
and
:$(\text b)\quad$if $\mathscr C$ satisfies circuit axioms (formulation 2) then $\mathscr C$ is the set of circuits of a matroid
Theorem: Circuits of Matroid iff Matroid Circuit Axioms/Circuits of Matroid implies Formulation 1

Let $S$ be a finite set.
Let $\mathscr C$ be a non-empty set of subsets of $S$.
Let $\mathscr C$ be the set of circuits of a matroid $M = \struct{S, \mathscr I}$ on $S$
Then:
:$\mathscr C$ satisfies the circuit axioms:
{{:Axiom:Circuit Axioms (Matroid)/Formulation 1}}

Proof:
==== $\mathscr C$ satisfies $(\text C 1)$ ====
By definition of circuit of a matroid:
:for all $C \in \mathscr C: C$ is a dependent subset
By definition of a dependent subset:
:for all $C \in \mathscr C$, $C \notin \mathscr I$
By definition of a matroid:
:$\O \in \mathscr I$
Hence:
:$\O \notin \mathscr C$
It follows that $\mathscr C$ satisfies circuit axiom $(\text C 1)$.
{{qed|lemma}}
==== $\mathscr C$ satisfies $(\text C 2)$ ====
Let $C_1, C_2 \in \mathscr C : C_1 \neq C_2$.
By definition of circuit of a matroid:
:$C_2$ is a dependent subset of $S$ which is a minimal dependent subset
and
:$C_1$ is a dependent subset
Hence:
:$C_1 \nsubseteq C_2$
It follows that $\mathscr C$ satisfies circuit axiom $(\text C 2)$.
{{qed|lemma}}
==== $\mathscr C$ satisfies $(\text C 3)$ ====
Let $\rho$ denote the rank function of the matroid $M$.
{{AimForCont}} $C_1, C_2 \in \mathscr C:$
:$C_1 \neq C_2$
and
:$\exists z \in C_1 \cap C_2 : \nexists C_3 \in \mathscr C : C_3 \subseteq \paren{C_1 \cup C_2} \setminus \set z$
From Proper Subset of Matroid Circuit is Independent:
:$\paren{C_1 \cup C_2} \setminus \set z$ is an independent subset.
Similarly:
:$\paren{C_1 \cap C_2}$ is an independent subset.
We have:
{{begin-eqn}}
{{eqn | l = \map \rho {C_1 \cup C_2}
      | o = \le
      | r = \map \rho {C_1} + \map \rho {C_2} - \map \rho {C_1 \cap C_2}
      | c = Rank axiom $(\text R 6)$
}}
{{eqn | r = \paren{\size {C_1} - 1} + \paren{\size {C_2} - 1} - \map \rho {C_1 \cap C_2}
      | c = Rank of Matroid Circuit is One Less Than Cardinality
}}
{{eqn | r = \size {C_1} + \size {C_2} - 2 - \map \rho {C_1 \cap C_2}
      | c = Rank of Matroid Circuit is One Less Than Cardinality
}}
{{eqn | r = \size {C_1 \cup C_2} + \size {C_1 \cap C_2} - 2 - \map \rho {C_1 \cap C_2}
      | c = Cardinality of Set Union
}}
{{eqn | r = \size {C_1 \cup C_2} + \size {C_1 \cap C_2} - 2 - \size {C_1 \cap C_2}
      | c = Rank of Independent Subset Equals Cardinality
}}
{{eqn | r = \size {C_1 \cup C_2} - 2
      | c = Cancelling terms
}}
{{eqn | r = \size {C_1 \cup C_2} - \size { \set z} - 1
      | c = Cardinality of Singleton
}}
{{eqn | r = \size {\paren{C_1 \cup C_2} \setminus \set z} - 1
      | c = Cardinality of Set Difference with Subset
}}
{{eqn | r = \map \rho {\paren{C_1 \cup C_2} \setminus \set z} - 1
      | c = Rank of Independent Subset Equals Cardinality
}}
{{eqn | r = \map \rho {\paren{C_1 \cup C_2} } - 1
      | o = \le
      | c = Rank Function is Increasing
}}
{{end-eqn}}
This is a contradiction.
It follows that $\mathscr C$ satisfies circuit axiom $(\text C 3)$.
Theorem: Equivalence of Definitions of Matroid Circuit Axioms/Formulation 1 Implies Formulation 2

Let $S$ be a finite set.
Let $\mathscr C$ be a non-empty set of subsets of $S$.
Let $\mathscr C$ satisfy the circuit axioms  (formulation 1):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 1}}
Then:
:$\mathscr C$ satisfies the circuit axioms (formulation 2):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 2}}

Proof:
Let $\mathscr C$ satisfy the circuit axioms $(\text C 1)$, $(\text C 2)$ and $(\text C 3)$.
It has only to be shown that circuit axiom $(\text C 4)$ is satisfied by $\mathscr C$.
Let:
{{begin-eqn}}
{{eqn | l = F = \leftset{\tuple{C, D, x, y} }
      | o = :
      | r = C, D \in \mathscr C \land C \neq D 
}}
{{eqn | o = \land
      | r = x \in C \cap D \land y \in C \setminus D
}}
{{eqn | o = \land
      | r = \nexists C' \in \mathscr C : y \in C' \subseteq \paren{C \cup D} \setminus \set x \mathop {\rightset {} } 
}}
{{end-eqn}}
To show that $\mathscr C$ satisfies circuit axiom $(\text C 4)$, it needs to be shown that $F = \O$.
{{AimForCont}} :
:$F \neq \O$
Let $\tuple{C_1, C_2, z, w} \in F$ :
:$\size{C_1 \cup C_2} = \min \set{\size{C \cup D} : \tuple{C, D, x, y} \in F}$
By circuit axiom $(\text C 3)$:
:$\exists C_3 \in \mathscr C : C_3 \subseteq \paren{C_1 \cup C_2} \setminus \set z$
By assumptiom:
:$w \notin C_3$
Consider $C_3 \cap \paren{C_2 \setminus C_1}$.
By circuit axiom $(\text C 2)$:
:$C_3 \nsubseteq C_1$
From Set Difference and Intersection form Partition:
:$C_3 \cap \paren{C_2 \setminus C_1} \neq \O$
Let $x \in C_3 \cap \paren{C_2 \setminus C_1}$.
We have:
:$x \in C_3 \cap C_2$
and
:$z \in C_2 \setminus C_3$
and
:$w \notin C_2 \cup C_3$
From Set is Subset of Union and Union of Subsets is Subset:
:$C_2 \cup C_3 \subseteq \C_1 \cup C_2$
Since $w \notin C_2 \cup C_3$:
:$C_2 \cup C_3$ is a proper subset of $C_1 \cup C_2$
By circuit axiom $(\text C 3)$ and the minimality of $C_1 \cup C_2$:
:$\exists C_4 \in \mathscr C : z \in C_4 \subseteq \paren{C_2 \cup C_3} \setminus \set{x}$
Now consider $C_1$ and $C_4$, we have:
:$z \in C_1 \cap C_4$
Since $w \notin C_2 \cup C_3$ then:
:$w \in C_1 \setminus C_4$
We have:
:$C_4 \subset C_2 \cup C_3 \subset C_1 \cup C_2$
From Set is Subset of Union and Union of Subsets is Subset:
:$C_1 \cup C_4 \subseteq C_1 \cup C_2$
Recall $x \in C_3 \cap \paren{C_2 \setminus C_1}$, then:
:$x \in C_2$
and
:$x \notin C_1$
Since $C_4 \subseteq \paren{C_2 \cup C_3} \setminus \set{x}$, then:
:$x \notin C_4$
It follows that:
:$x \notin C_1 \cup C_4$
and
:$x \in C_1 \cup C_2$
Hence:
:$C_1 \cup C_4$ is a proper subset of $C_1 \cup C_2$
By circuit axiom $(\text C 3)$ and the minimality of $C_1 \cup C_2$:
:$\exists C_5 \in \mathscr C : w \in C_5 \subseteq \paren{C_1 \cup C_4} \setminus \set{z}$
Since $C_1 \cup C_4 \subset C_1 \cup C_2$, then we have found $C_5$ such that:
:$w \in C_5 \subseteq \paren{C_1 \cup C_2} \setminus \set{z}$
This contradicts the fact that $\tuple{C_1, C_2, z, w} \in F$.
It follows that circuit axiom $(\text C 4)$ is satisfied.
Theorem: Equivalence of Definitions of Matroid Circuit Axioms/Formulation 1 Implies Formulation 3

Let $S$ be a finite set.
Let $\mathscr C$ be a non-empty set of subsets of $S$.
Let $\mathscr C$ satisfy the circuit axioms (formulation 1):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 1}}
Then:
:$\mathscr C$ satisfies the circuit axioms (formulation 3):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 3}}

Proof:
Let $\mathscr C$ satisfy the circuit axioms $(\text C 1)$, $(\text C 2)$ and $(\text C 3)$.
We need to show that $\mathscr C$ satisfies circuit axiom:
{{begin-axiom}}
{{axiom | n = \text C 5
        | q = \forall X \subseteq S \land \forall x \in S 
        | mr = \paren {\forall C \in \mathscr C : C \nsubseteq X} \implies \paren {\exists \text{ at most one } C \in \mathscr C : C \subseteq X \cup \set x}
}}
{{end-axiom}}
Let $X \subset S : \forall C \in \mathscr C : C \nsubseteq X$.
Let $x \in S$.
{{AimForCont}}:
:$\exists C_1, C_2 \in \mathscr C : C_1 \neq C_2 : C_1, C_2 \subseteq X \cup \set x$.
Since $C_1, C_2 \nsubseteq X$ then:
:$x \in C_1 \cap C_2$
From circuit axiom $(\text C 3)$:
:$\exists C_3 \in \mathscr C : C_3 \subseteq \paren{C_1 \cup C_2} \setminus \set x$
We have:
:$\paren{C_1 \cup C_2} \setminus \set x \subseteq X$
Hence:
:$C_3 \subseteq X$
This contradicts the assumption that:
:$X \subset S : \forall C \in \mathscr C : C \nsubseteq X$
It follows that:
:$\exists \text{ at most one } C \in \mathscr C : C \subseteq X \cup \set x$
It follows that $\mathscr C$ satisfies circuit axiom $(\text C 5)$.