let V be Z_Module; :: thesis: for W1, W2, W3 being Submodule of V holds W1 /\ W2 is Submodule of (W1 + W3) /\ W2
let W1, W2, W3 be Submodule of V; :: thesis: W1 /\ W2 is Submodule of (W1 + W3) /\ W2
for v being VECTOR of V st v in W1 /\ W2 holds
v in (W1 + W3) /\ W2

proof

let v be VECTOR of V; :: thesis: ( v in W1 /\ W2 implies v in (W1 + W3) /\ W2 )
assume A1: v in W1 /\ W2 ; :: thesis: v in (W1 + W3) /\ W2
v in W1 by A1, ZMODUL01:94;
then A2: v in W1 + W3 by ZMODUL01:93;
v in W2 by A1, ZMODUL01:94;
hence v in (W1 + W3) /\ W2 by A2, ZMODUL01:94; :: thesis: verum

end;

hence W1 /\ W2 is Submodule of (W1 + W3) /\ W2 by ZMODUL01:44; :: thesis: verum