let R be Ring; :: thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds
( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )
let V be RightMod of R; :: thesis: for W1, W2 being Submodule of V holds
( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )
let W1, W2 be Submodule of V; :: thesis: ( W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2 )
the carrier of (W1 /\ W2) c= the carrier of W1 by Lm6;
hence W1 /\ W2 is Submodule of W1 by RMOD_2:27; :: thesis: W1 /\ W2 is Submodule of W2
the carrier of (W2 /\ W1) c= the carrier of W2 by Lm6;
then the carrier of (W1 /\ W2) c= the carrier of W2 by Th14;
hence W1 /\ W2 is Submodule of W2 by RMOD_2:27; :: thesis: verum