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

Rnk A <= Rnk B

let A, B be Subset of M; :: thesis: ( A c= B implies Rnk A <= Rnk B )

ex C being independent Subset of M st

( C c= A & card C = Rnk A ) by Th18;

hence ( A c= B implies Rnk A <= Rnk B ) by Th17, XBOOLE_1:1; :: thesis: verum

Rnk A <= Rnk B

let A, B be Subset of M; :: thesis: ( A c= B implies Rnk A <= Rnk B )

ex C being independent Subset of M st

( C c= A & card C = Rnk A ) by Th18;

hence ( A c= B implies Rnk A <= Rnk B ) by Th17, XBOOLE_1:1; :: thesis: verum