let R be Ring; :: thesis: for V being RightMod of R
for W being strict Submodule of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
let V be RightMod of R; :: thesis: for W being strict Submodule of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
let W be strict Submodule of V; :: thesis: ( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
( the carrier of (((Omega). V) /\ W) = the carrier of V /\ the carrier of W & the carrier of W c= the carrier of V ) by Def2, RMOD_2:def 2;
hence ((Omega). V) /\ W = W by RMOD_2:29, XBOOLE_1:28; :: thesis: W /\ ((Omega). V) = W
hence W /\ ((Omega). V) = W by Th14; :: thesis: verum