let M be finite-degree Matroid; :: thesis: for A being Subset of M
for e being Element of M holds
( e in Span A iff Rnk (A \/ {e}) = Rnk A )
let A be Subset of M; :: thesis: for e being Element of M holds
( e in Span A iff Rnk (A \/ {e}) = Rnk A )
let e be Element of M; :: thesis: ( e in Span A iff Rnk (A \/ {e}) = Rnk A )

hereby :: thesis: ( Rnk (A \/ {e}) = Rnk A implies e in Span A )

assume e in Span A ; :: thesis: Rnk (A \/ {e}) = Rnk A
then ex x being Element of M st
( e = x & x is_dependent_on A ) ;
hence Rnk (A \/ {e}) = Rnk A ; :: thesis: verum

end;

assume Rnk (A \/ {e}) = Rnk A ; :: thesis: e in Span A
then e is_dependent_on A ;
hence e in Span A ; :: thesis: verum