theorem :: RUSUB_2:61

for V being RealUnitarySpace
for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Lm12;