let R be Ring; :: thesis: for V being RightMod of R
for W1, W2 being Submodule of V holds
( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) iff ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
let V be RightMod of R; :: thesis: for W1, W2 being Submodule of V holds
( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) iff ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
let W1, W2 be Submodule of V; :: thesis: ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) iff ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
thus ( for W being Submodule of V holds not the carrier of W = the carrier of W1 \/ the carrier of W2 or W1 is Submodule of W2 or W2 is Submodule of W1 ) :: thesis: ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )

proof

given W being Submodule of V such that A1: the carrier of W = the carrier of W1 \/ the carrier of W2 ; :: thesis: ( W1 is Submodule of W2 or W2 is Submodule of W1 )
set VW = the carrier of W;
assume that
A2: W1 is not Submodule of W2 and
A3: W2 is not Submodule of W1 ; :: thesis: contradiction
not the carrier of W2 c= the carrier of W1 by A3, RMOD_2:27;
then consider y being object such that
A4: y in the carrier of W2 and
A5: not y in the carrier of W1 ;
reconsider y = y as Element of the carrier of W2 by A4;
reconsider y = y as Vector of V by RMOD_2:10;
reconsider A1 = the carrier of W as Subset of V by RMOD_2:def 2;
A6: A1 is linearly-closed by RMOD_2:33;
not the carrier of W1 c= the carrier of W2 by A2, RMOD_2:27;
then consider x being object such that
A7: x in the carrier of W1 and
A8: not x in the carrier of W2 ;
reconsider x = x as Element of the carrier of W1 by A7;
reconsider x = x as Vector of V by RMOD_2:10;

A9: now :: thesis: not x + y in the carrier of W2

reconsider A2 = the carrier of W2 as Subset of V by RMOD_2:def 2;
A10: A2 is linearly-closed by RMOD_2:33;
assume x + y in the carrier of W2 ; :: thesis: contradiction
then (x + y) - y in the carrier of W2 by A10, RMOD_2:3;
then x + (y - y) in the carrier of W2 by RLVECT_1:def 3;
then x + (0. V) in the carrier of W2 by VECTSP_1:19;
hence contradiction by A8, RLVECT_1:def 4; :: thesis: verum

end;

A11: now :: thesis: not x + y in the carrier of W1

reconsider A2 = the carrier of W1 as Subset of V by RMOD_2:def 2;
A12: A2 is linearly-closed by RMOD_2:33;
assume x + y in the carrier of W1 ; :: thesis: contradiction
then (y + x) - x in the carrier of W1 by A12, RMOD_2:3;
then y + (x - x) in the carrier of W1 by RLVECT_1:def 3;
then y + (0. V) in the carrier of W1 by VECTSP_1:19;
hence contradiction by A5, RLVECT_1:def 4; :: thesis: verum

end;

( x in the carrier of W & y in the carrier of W ) by A1, XBOOLE_0:def 3;
then x + y in the carrier of W by A6;
hence contradiction by A1, A11, A9, XBOOLE_0:def 3; :: thesis: verum

end;

A13: now :: thesis: ( W1 is Submodule of W2 & ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )

assume W1 is Submodule of W2 ; :: thesis: ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then the carrier of W1 c= the carrier of W2 by RMOD_2:def 2;
then the carrier of W1 \/ the carrier of W2 = the carrier of W2 by XBOOLE_1:12;
hence ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; :: thesis: verum

end;

A14: now :: thesis: ( W2 is Submodule of W1 & ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )

assume W2 is Submodule of W1 ; :: thesis: ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then the carrier of W2 c= the carrier of W1 by RMOD_2:def 2;
then the carrier of W1 \/ the carrier of W2 = the carrier of W1 by XBOOLE_1:12;
hence ( ( W1 is Submodule of W2 or W2 is Submodule of W1 ) implies ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; :: thesis: verum

end;

assume ( W1 is Submodule of W2 or W2 is Submodule of W1 ) ; :: thesis: ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2
hence ex W being Submodule of V st the carrier of W = the carrier of W1 \/ the carrier of W2 by A13, A14; :: thesis: verum