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 object ; :: 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
A1: x = e and
A2: e is_dependent_on Span A ;
e is_dependent_on A by A2, Th34;
hence x in Span A by A1; :: thesis: verum
end;
thus not Span A c/= Span (Span A) by Th31; :: thesis: verum