theorem :: RLSUB_2:21

for V being strict RealLinearSpace holds ((Omega). V) /\ ((Omega). V) = V by Th20;