let R be Ring; :: thesis: for V being RightMod of R
for W1 being Submodule of V
for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let V be RightMod of R; :: thesis: for W1 being Submodule of V
for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W1 be Submodule of V; :: thesis: for W2 being strict Submodule of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W2 be strict Submodule of V; :: thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 )
assume A1: the carrier of W1 c= the carrier of W2 ; :: thesis: W1 + W2 = W2
A2: the carrier of (W1 + W2) c= the carrier of W2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of W2 )
assume x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of W2
then x in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } by Def1;
then consider u, v being Vector of V such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2 ;
W1 is Submodule of W2 by A1, RMOD_2:27;
then v in W2 by A4, RMOD_2:8;
then v + u in W2 by A5, RMOD_2:20;
hence x in the carrier of W2 by A3; :: thesis: verum

end;

W1 + W2 = W2 + W1 by Lm1;
then the carrier of W2 c= the carrier of (W1 + W2) by Lm2;
then the carrier of (W1 + W2) = the carrier of W2 by A2;
hence W1 + W2 = W2 by RMOD_2:29; :: thesis: verum