let GF be Field; :: thesis: for V being VectSp of GF
for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
let V be VectSp of GF; :: 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 VECTSP_7:def 3;
then reconsider B = A as linearly-independent Subset of V by Th11;
consider I being Basis of V such that
A1: B c= I by VECTSP_7:19;
take I ; :: thesis: A c= I
thus A c= I by A1; :: thesis: verum