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