theorem :: RLSUB_1:41

for V being strict RealLinearSpace holds V is Subspace of (Omega). V ;