let M be finite-degree Matroid; for A being Subset of M holds Rnk (Span A) = Rnk A
let A be Subset of M; Rnk (Span A) = Rnk A
consider Ca being independent Subset of M such that
A1:
Ca c= A
and
A2:
card Ca = Rnk A
by Th18;
A c= Span A
by Th31;
then
Ca c= Span A
by A1;
then consider C being independent Subset of M such that
A3:
Ca c= C
and
A4:
C is_maximal_independent_in Span A
by Th14;
now not C c/= Caassume
C c/= Ca
;
contradictionthen consider x being
object such that A5:
x in C
and A6:
x nin Ca
;
C c= Span A
by A4;
then
x in Span A
by A5;
then consider e being
Element of
M such that A7:
x = e
and A8:
e is_dependent_on A
;
{e} c= C
by A5, A7, ZFMISC_1:31;
then
Ca \/ {e} c= C
by A3, XBOOLE_1:8;
then reconsider Ce =
Ca \/ {e} as
independent Subset of
M by Th3;
Ce c= A \/ {e}
by A1, XBOOLE_1:9;
then consider D being
independent Subset of
M such that A9:
Ce c= D
and A10:
D is_maximal_independent_in A \/ {e}
by Th14;
card Ca =
Rnk (A \/ {e})
by A2, A8
.=
card D
by A10, Th19
;
then A11:
card Ce <= card Ca
by A9, NAT_1:43;
card Ca <= card Ce
by NAT_1:43, XBOOLE_1:7;
then
card Ca = card Ce
by A11, XXREAL_0:1;
then
Ca = Ce
by CARD_2:102, XBOOLE_1:7;
then
e nin {e}
by A6, A7, XBOOLE_0:def 3;
hence
contradiction
by TARSKI:def 1;
verum end;
then
C = Ca
by A3;
hence
Rnk (Span A) = Rnk A
by A2, A4, Th19; verum