let M be finite-degree Matroid; :: thesis: for A being Subset of M holds A c= Span A

let A be Subset of M; :: thesis: A c= Span A

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A or e in Span A )

assume A1: e in A ; :: thesis: e in Span A

then reconsider x = e as Element of M ;

x is_dependent_on A by A1, Th28;

hence e in Span A ; :: thesis: verum

let A be Subset of M; :: thesis: A c= Span A

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A or e in Span A )

assume A1: e in A ; :: thesis: e in Span A

then reconsider x = e as Element of M ;

x is_dependent_on A by A1, Th28;

hence e in Span A ; :: thesis: verum