theorem :: RLSUB_2:33

for V being strict RealLinearSpace holds V in Subspaces V