let M be finite-degree Matroid; :: thesis: for A being independent Subset of M ex B being Basis of M st A c= B
let A be independent Subset of M; :: thesis: ex B being Basis of M st A c= B
consider B being independent Subset of M such that
A1: ( A c= B & B is_maximal_independent_in [#] M ) by Th;
reconsider B = B as Basis of M by A1, BASIS;
take B ; :: thesis: A c= B
thus A c= B by A1; :: thesis: verum