let R be Ring; :: thesis: for V being RightMod of R
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 /\ W3 is Submodule of W2 /\ W3
let V be RightMod of R; :: thesis: for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 holds
W1 /\ W3 is Submodule of W2 /\ W3
let W1, W2, W3 be Submodule of V; :: thesis: ( W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3 )
set A1 = the carrier of W1;
set A2 = the carrier of W2;
set A3 = the carrier of W3;
set A4 = the carrier of (W1 /\ W3);
assume W1 is Submodule of W2 ; :: thesis: W1 /\ W3 is Submodule of W2 /\ W3
then the carrier of W1 c= the carrier of W2 by RMOD_2:def 2;
then the carrier of W1 /\ the carrier of W3 c= the carrier of W2 /\ the carrier of W3 by XBOOLE_1:26;
then the carrier of (W1 /\ W3) c= the carrier of W2 /\ the carrier of W3 by Def2;
then the carrier of (W1 /\ W3) c= the carrier of (W2 /\ W3) by Def2;
hence W1 /\ W3 is Submodule of W2 /\ W3 by RMOD_2:27; :: thesis: verum