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

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