let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W1, W2 being Subspace of M holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for W1, W2 being Subspace of M holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
let W1, W2 be Subspace of M; :: thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M 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 Subspace of M holds not the carrier of W = the carrier of W1 \/ the carrier of W2 or W1 is Subspace of W2 or W2 is Subspace of W1 ) :: thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )

proof

given W being Subspace of M such that A1: the carrier of W = the carrier of W1 \/ the carrier of W2 ; :: thesis: ( W1 is Subspace of W2 or W2 is Subspace of W1 )
set VW = the carrier of W;
assume ( W1 is not Subspace of W2 & W2 is not Subspace of W1 ) ; :: thesis: contradiction
then A2: ( not the carrier of W1 c= the carrier of W2 & not the carrier of W2 c= the carrier of W1 ) by VECTSP_4:35;
then consider x being set such that
A3: x in the carrier of W1 and
A4: not x in the carrier of W2 by TARSKI:def 3;
consider y being set such that
A5: y in the carrier of W2 and
A6: not y in the carrier of W1 by A2, TARSKI:def 3;
reconsider x = x as Element of the carrier of W1 by A3;
reconsider x = x as Element of M by VECTSP_4:18;
reconsider y = y as Element of the carrier of W2 by A5;
reconsider y = y as Element of M by VECTSP_4:18;
reconsider A1 = the carrier of W as Subset of M by VECTSP_4:def 2;
( x in the carrier of W & y in the carrier of W & A1 is linearly-closed ) by A1, VECTSP_4:41, XBOOLE_0:def 3;
then A7: x + y in the carrier of W by VECTSP_4:def 1;

A8: now

assume A9: x + y in the carrier of W1 ; :: thesis: contradiction
reconsider A2 = the carrier of W1 as Subset of M by VECTSP_4:def 2;
A2 is linearly-closed by VECTSP_4:41;
then (y + x) - x in the carrier of W1 by A9, VECTSP_4:6;
then y + (x - x) in the carrier of W1 by RLVECT_1:def 6;
then y + (0. M) in the carrier of W1 by VECTSP_1:66;
hence contradiction by A6, RLVECT_1:10; :: thesis: verum

end;

now

assume A10: x + y in the carrier of W2 ; :: thesis: contradiction
reconsider A2 = the carrier of W2 as Subset of M by VECTSP_4:def 2;
A2 is linearly-closed by VECTSP_4:41;
then (x + y) - y in the carrier of W2 by A10, VECTSP_4:6;
then x + (y - y) in the carrier of W2 by RLVECT_1:def 6;
then x + (0. M) in the carrier of W2 by VECTSP_1:66;
hence contradiction by A4, RLVECT_1:10; :: thesis: verum

end;

hence contradiction by A1, A7, A8, XBOOLE_0:def 3; :: thesis: verum

end;

assume A11: ( W1 is Subspace of W2 or W2 is Subspace of W1 ) ; :: thesis: ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2

A12: now

assume W1 is Subspace of W2 ; :: thesis: ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2
then the carrier of W1 c= the carrier of W2 by VECTSP_4:def 2;
then the carrier of W1 \/ the carrier of W2 = the carrier of W2 by XBOOLE_1:12;
hence ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 ; :: thesis: verum

end;

now

assume W2 is Subspace of W1 ; :: thesis: ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2
then the carrier of W2 c= the carrier of W1 by VECTSP_4:def 2;
then the carrier of W1 \/ the carrier of W2 = the carrier of W1 by XBOOLE_1:12;
hence ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 ; :: thesis: verum

end;

hence ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 by A11, A12; :: thesis: verum