let M be finite-degree Matroid; :: thesis: for A being Subset of M holds Span (Span A) = Span A
let A be Subset of M; :: thesis: Span (Span A) = Span A
thus Span (Span A) c= Span A :: according to XBOOLE_0:def 10 :: thesis: not Span A c/= Span (Span A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Span (Span A) or x in Span A )
assume x in Span (Span A) ; :: thesis: x in Span A
then consider e being Element of M such that
A0: ( x = e & e is_dependent_on Span A ) ;
e is_dependent_on A by A0, Sd;
hence x in Span A by A0; :: thesis: verum

end;

thus not Span A c/= Span (Span A) by S1; :: thesis: verum