theorem Th22: :: RMOD_3:22
for R being Ring
for V being RightMod of R
for W being strict Submodule of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )