theorem Th16: :: RLVECT_5:16

for V being RealLinearSpace
for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B