let V be RealLinearSpace; :: thesis: for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
let W be Subspace of V; :: thesis: for A being Basis of W ex B being Basis of V st A c= B
let A be Basis of W; :: thesis: ex B being Basis of V st A c= B
A is linearly-independent by RLVECT_3:def 3;
then A is linearly-independent Subset of V by Th14;
then consider I being Basis of V such that
A1: A c= I by Th2;
take I ; :: thesis: A c= I
thus A c= I by A1; :: thesis: verum