theorem :: RLSUB_2:62

for V being RealLinearSpace
for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm12;