let M be finite-degree Matroid; :: thesis: for A being Subset of M holds Rnk (Span A) = Rnk A
let A be Subset of M; :: thesis: Rnk (Span A) = Rnk A
A0: A c= Span A by S1;
consider Ca being independent Subset of M such that
B2: ( Ca c= A & card Ca = Rnk A ) by ThR1;
Ca c= Span A by A0, B2, XBOOLE_1:1;
then consider C being independent Subset of M such that
A2: ( Ca c= C & C is_maximal_independent_in Span A ) by Th;

now

assume C c/= Ca ; :: thesis: contradiction
then consider x being set such that
A3: ( x in C & x nin Ca ) by TARSKI:def 3;
C c= Span A by A2, ThR2;
then x in Span A by A3;
then consider e being Element of M such that
A4: ( x = e & e is_dependent_on A ) ;
{e} c= C by A3, A4, ZFMISC_1:37;
then Ca \/ {e} c= C by A2, XBOOLE_1:8;
then reconsider Ce = Ca \/ {e} as independent Subset of M by M1;
Ce c= A \/ {e} by B2, XBOOLE_1:9;
then consider D being independent Subset of M such that
A6: ( Ce c= D & D is_maximal_independent_in A \/ {e} ) by Th;
card Ca = Rnk (A \/ {e}) by B2, A4, DF
.= card D by A6, ThR2 ;
then ( card Ce <= card Ca & card Ca <= card Ce ) by A6, XBOOLE_1:7, NAT_1:44;
then card Ca = card Ce by XXREAL_0:1;
then Ca = Ce by XBOOLE_1:7, CARD_FIN:1;
then e nin {e} by A3, A4, XBOOLE_0:def 3;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then C = Ca by A2, XBOOLE_0:def 10;
hence Rnk (Span A) = Rnk A by B2, A2, ThR2; :: thesis: verum