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 and
A2: B is_maximal_independent_in [#] M by Th14;
reconsider B = B as Basis of M by A2, Def12;
take B ; :: thesis: A c= B
thus A c= B by A1; :: thesis: verum