let M be finite-degree Matroid; :: thesis: for A, B being Subset of M st A c= B holds
Span A c= Span B
let A, B be Subset of M; :: thesis: ( A c= B implies Span A c= Span B )
assume A1: A c= B ; :: thesis: Span A c= Span B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Span A or x in Span B )
assume x in Span A ; :: thesis: x in Span B
then ex e being Element of M st
( x = e & e is_dependent_on A ) ;
then ex e being Element of M st
( x = e & e is_dependent_on B ) by A1, Th29;
hence x in Span B ; :: thesis: verum