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 A1: Rnk ((Span A) \/ {e}) = Rnk (Span A) ; :: according to MATROID0:def 14 :: thesis: e is_dependent_on A
A2: Rnk A = Rnk (Span A) by Th33;
consider Ca being independent Subset of M such that
A3: Ca c= A and
A4: card Ca = Rnk A by Th18;
A5: Rnk A = Rnk Ca by A4, Th21;
A6: Rnk Ca <= Rnk (A \/ {e}) by A3, Th24, XBOOLE_1:10;
A c= Span A by Th31;
then Rnk (A \/ {e}) <= Rnk A by A1, A2, Th24, XBOOLE_1:9;
hence Rnk (A \/ {e}) = Rnk A by A5, A6, XXREAL_0:1; :: according to MATROID0:def 14 :: thesis: verum