Theorem: Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom/Lemma 1

:$\exists B_3 \in \mathscr B$:
::$V \subseteq B_3$
::$\card{B_1 \cap B_3} > \card{B_1 \cap B_2}$

Proof:
=== Lemma 2 ===
{{:Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom/Lemma 2}}{{qed|lemma}}
From Larger Set has Larger Set Difference:
:$(1):\quad \card {V \setminus U} < \card {U \setminus V}$
We have:
{{begin-eqn}}
{{eqn | l = \card {B_1}
      | r = \card{ \paren{B_1 \cap B_2} \cup \paren{B_1 \setminus B_2} }
      | c = Set Difference Union Intersection
}}
{{eqn | n = 2
      | r = \card{B_1 \cap B_2} + \card{B_1 \setminus B_2}
      | c = Set Difference and Intersection are Disjoint and {{Corollary|Cardinality of Set Union}}
}}
{{end-eqn}}
and
{{begin-eqn}}
{{eqn | l = \card {B_2}
      | r = \card{ \paren{B_2 \cap B_1} \cup \paren{B_2 \setminus B_1} }
      | c = Set Difference Union Intersection
}}
{{eqn | r = \card{B_2 \cap B_1} + \card{B_2 \setminus B_1}
      | c = Set Difference and Intersection are Disjoint and {{Corollary|Cardinality of Set Union}}
}}
{{eqn | r = \card{B_2 \cap B_1} + \card{\paren{\paren{B_2 \setminus B_1} \cap V} \cup \paren{\paren{B_2 \setminus B_1} \setminus V} }
      | c = Set Difference Union Intersection
}}
{{eqn | r = \card{B_2 \cap B_1} + \card{\paren{B_2 \setminus B_1} \cap V} + \card{\paren{B_2 \setminus B_1} \setminus V}
      | c = Set Difference and Intersection are Disjoint and {{Corollary|Cardinality of Set Union}}
}}
{{eqn | n = 3
      | r = \card{B_2 \cap B_1} + \card{V \setminus B_1} + \card{\paren{B_2 \setminus B_1} \setminus V}
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{end-eqn}}
and
{{begin-eqn}}
{{eqn | l = U \setminus V
      | o = \subseteq
      | r = U
}}
{{eqn | o = \subseteq
      | r = B_1
}}
{{eqn | ll = \leadsto
      | l = U \setminus V
      | o = \subseteq
      | r = B_1 \setminus B_2
      | c = Subset of Set Difference iff Disjoint Set and $B_2 \cap \paren{U \setminus V} = \O$
}}
{{eqn | n = 4
      | ll = \leadsto
      | l = \card{U \setminus V}
      | o = \le
      | r = \card{B_1 \setminus B_2}
      | c = Cardinality of Subset of Finite Set
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = 0
      | r = \card{B_2} - \card{B_1}
      | c = Lemma 2
}}
{{eqn | r = \card{B_2 \cap B_1} + \card{V \setminus B_1} + \card{\paren{B_2 \setminus B_1} \setminus V}  - \card{B_1 \cap B_2} - \card{B_1 \setminus B_2}
      | c = from $(2)$ and $(3)$
}}
{{eqn | r = \card{V \setminus B_1} + \card{\paren{B_2 \setminus B_1} \setminus V} - \card{B_1 \setminus B_2}
      | c = Canceling terms
}}
{{eqn | o = \le 
      | r = \card{V \setminus B_1} + \card{\paren{B_2 \setminus B_1} \setminus V} - \card{U \setminus V}
      | c = from $(4)$
}}
{{eqn | o = < 
      | r = \card{V \setminus B_1} + \card{\paren{B_2 \setminus B_1} \setminus V} - \card{V \setminus U}
      | c = from $(1)$
}}
{{eqn | o = \le 
      | r = \card{V \setminus B_1} + \card{\paren{B_2 \setminus B_1} \setminus V} - \card{V \setminus B_1}
      | c = As $U \subseteq B_1$
}}
{{eqn | r = \card{\paren{B_2 \setminus B_1} \setminus V}
      | c = Canceling terms
}}
{{end-eqn}}
From the contrapositive statement of Cardinality of Empty Set:
:$\paren{B_2 \setminus B_1} \setminus V \ne \O$
Hence:
:$\exists y \in \paren{B_2 \setminus B_1} \setminus V$
From $(\text B 1)$:
:$\exists z \in B_1 \setminus B_2 : \paren{B_2 \setminus \set y} \cup \set z \in \mathscr B$
Let:
:$B_3 = \paren{B_2 \setminus \set y} \cup \set z$
We have:
:{{begin-eqn}}
{{eqn | l = V
      | o = \subseteq
      | r = B_2 \setminus \set y
      | c = As $y \notin V$ and $V \subseteq B_2$
}}
{{eqn | o = \subseteq
      | r = \paren{B_2 \setminus \set y} \cup \set z
      | c = Set is Subset of Union
}}
{{eqn | r = B_3
}}
{{end-eqn}}
From Finite Set Formed by Substitution has Larger Intersection:
:$\card{B_1 \cap B_3} = \card{B_1 \cap B_2} + 1$
Hence:
:$\card{B_1 \cap B_3} > \card{B_1 \cap B_2}$
{{qed}}
Category:Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom
rcb2uu61gs74sb8edyedtytrqegpaj4