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

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