let V be RealUnitarySpace; :: 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 Def2;
then reconsider B = A as linearly-independent Subset of V by Th22;
consider I being Basis of V such that
A1: B c= I by Th15;
take I ; :: thesis: A c= I
thus A c= I by A1; :: thesis: verum