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)

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

thus
not Span A c/= Span (Span A)
by Th31; :: thesis: verum
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;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