Theorem: Circuits of Matroid iff Matroid Circuit Axioms/Formulation 2 implies Circuits of Matroid

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

Proof:
We will define a mapping $\rho$ associated with $\mathscr C$.
It will be shown that $\rho$ is the rank function of a matroid $M$ which has $\mathscr C$ as the set of circuits.
For any ordered tuple $\tuple{x_1, \ldots, x_q}$ of elements of $S$, let $\map \theta {x_1, \ldots, x_q}$ be the ordered tuple defined by:
:$\forall i \in \set{1, \ldots, q} : \map \theta {x_1, \ldots, x_q}_i = \begin{cases} 0 & : \exists C \in \mathscr C : x_i \in C \subseteq \set{x_1, \ldots, x_i}\\ 1 & : \text {otherwise}  \end{cases}$
Let $t$ be the mapping from the set of ordered tuple of $S$ defined  by:
:$\map t {x_1, \ldots, x_q} = \ds \sum_{i = 1}^q \map \theta {x_1, \ldots, x_q}_i$
==== Lemma 1 ====
{{:Circuits of Matroid iff Matroid Circuit Axioms/Lemma 1}}{{qed|lemma}}
Let $\rho : \powerset S \to \Z$ be the mapping defined by:
:$\forall A \subseteq S$:
::$\map \rho A = \begin{cases} 0 & : \text{if } A = \O \\ \map t {x_1, \ldots, x_q } & : \text{if } A = \set{x_1, \ldots, x_q} \end{cases}$
From Lemma 1:
:$\rho$ is well-defined
We now show that $\rho$ satisfies the rank function axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
==== $\rho$ satisfies $(\text R 1)$ ====
Follows from the definition of $\rho$.
{{qed|lemma}}
==== $\rho$ satisfies $(\text R 2)$ ====
Let:
:$X = \set{x_1, \ldots, x_q} \subseteq S$ and $y \in S$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho {X \cup \set y} - \map \rho X
      | r = \map t {\tuple{x_1, \dots, x_q, y} } - \map t {\tuple{x_1, \dots, x_q} }
      | c = Definition of $\rho$
}}
{{eqn | r = \map \theta {\tuple{x_1, \dots, x_q, y} }_{q+1}
      | c = Definition of $t$
}}
{{eqn | r = \begin{cases} 0 & : \exists C \in \mathscr C : y \in C \subseteq \set{x_1, \ldots, x_q, y}\\ 1 & : \text {otherwise} \end{cases}
      | c = Definition of $\theta$
}}
{{eqn | ll = \leadstoandfrom
      | l = 0
      | o = \le
      | r = \map \rho {X \cup \set y} - \map \rho X \le 1
}}
{{eqn | ll = \leadstoandfrom
      | l = \map \rho X
      | o = \le
      | r = \map \rho {X \cup \set y} \le \map \rho X + 1
      | c = Adding $\map \rho X$ to all terms
}}
{{end-eqn}}
{{qed|lemma}}
==== Lemma 2 ====
{{:Circuits of Matroid iff Matroid Circuit Axioms/Lemma 2}}{{qed|lemma}}
==== $\rho$ satisfies $(\text R 3)$ ====
Let:
:$X \subseteq S$ and $y, z \in S$
Let:
:$\map \rho {X \cup \set y} = \map \rho {X \cup \set z} = \map \rho X$
===== Case 1 : $z \in X$ =====
Let $z \in X$.
Then:
:$\map \rho {X \cup \set {y,z}} = \map \rho {X \cup \set y}$
Since $\map \rho {X \cup \set y} = \map \rho X$, then:
:$\map \rho {X \cup \set {y,z}} = \map \rho X$
{{qed|lemma}}
===== Case 2 : $z = y$ =====
Let $z = y$.
Then
:$\map \rho {X \cup \set {y,z}} = \map \rho {X \cup \set y}$
Since $\map \rho {X \cup \set y} = \map \rho X$, then:
:$\map \rho {X \cup \set {y,z}} = \map \rho X$
{{qed|lemma}}
===== Case 3 : $z \neq y$ and $z \notin X$ =====
Let $z \neq y$ and $z \notin X$.
Then $z \notin X \cup \set y$.
From Lemma 2:
:$\exists C_z \in \mathscr C : z \in C_z \subseteq X \cup \set{z} \subseteq X \cup \set{y,z}$
From Lemma 2:
:$\map \rho {X \cup \set{y, z}} = \map \rho {X \cup \set y} = \map \rho X$ 
{{qed|lemma}}
From Matroid Rank Function Iff Matroid Rank Axioms:
:$\rho$ is the rank function of a matroid $M = \struct{S, \mathscr I}$ on $S$
==== Lemma 3 ====
{{:Circuits of Matroid iff Matroid Circuit Axioms/Lemma 3}}