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