let M be finite-degree Matroid; :: thesis: for A being Subset of M
for e being Element of M st e is_dependent_on Span A holds
e is_dependent_on A
let A be Subset of M; :: thesis: for e being Element of M st e is_dependent_on Span A holds
e is_dependent_on A
let e be Element of M; :: thesis: ( e is_dependent_on Span A implies e is_dependent_on A )
assume Z0: Rnk ((Span A) \/ {e}) = Rnk (Span A) ; :: according to MATROID0:def 14 :: thesis: e is_dependent_on A
consider Ca being independent Subset of M such that
B2: ( Ca c= A & card Ca = Rnk A ) by ThR1;
A0: A c= Span A by S1;
then Ca c= Span A by 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;
A3: ( Rnk A = Rnk (Span A) & Rnk (Span A) = card C & C c= Span A ) by A2, ThR2, S0;
( Ca c= A \/ {e} & A \/ {e} c= (Span A) \/ {e} ) by B2, A0, XBOOLE_1:9, XBOOLE_1:10;
then ( Rnk A = Rnk Ca & Rnk Ca <= Rnk (A \/ {e}) & Rnk (A \/ {e}) <= Rnk A ) by Z0, B2, R2, A3, ThR4;
hence Rnk (A \/ {e}) = Rnk A by XXREAL_0:1; :: according to MATROID0:def 14 :: thesis: verum