let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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 )

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

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 vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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 that

A2: W1 is not Subspace of W2 and

A3: W2 is not Subspace of W1 ; :: thesis: contradiction

not the carrier of W2 c= the carrier of W1 by A3, VECTSP_4: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 Element of M by VECTSP_4:10;

reconsider A1 = the carrier of W as Subset of M by VECTSP_4:def 2;

A6: A1 is linearly-closed by VECTSP_4:33;

not the carrier of W1 c= the carrier of W2 by A2, VECTSP_4: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 Element of M by VECTSP_4:10;

then x + y in the carrier of W by A6;

hence contradiction by A1, A11, A9, XBOOLE_0:def 3; :: thesis: verum

end;set VW = the carrier of W;

assume that

A2: W1 is not Subspace of W2 and

A3: W2 is not Subspace of W1 ; :: thesis: contradiction

not the carrier of W2 c= the carrier of W1 by A3, VECTSP_4: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 Element of M by VECTSP_4:10;

reconsider A1 = the carrier of W as Subset of M by VECTSP_4:def 2;

A6: A1 is linearly-closed by VECTSP_4:33;

not the carrier of W1 c= the carrier of W2 by A2, VECTSP_4: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 Element of M by VECTSP_4:10;

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

reconsider A2 = the carrier of W2 as Subset of M by VECTSP_4:def 2;

A10: A2 is linearly-closed by VECTSP_4:33;

assume x + y in the carrier of W2 ; :: thesis: contradiction

then (x + y) - y in the carrier of W2 by A10, VECTSP_4:3;

then x + (y - y) in the carrier of W2 by RLVECT_1:def 3;

then x + (0. M) in the carrier of W2 by VECTSP_1:19;

hence contradiction by A8, RLVECT_1:4; :: thesis: verum

end;A10: A2 is linearly-closed by VECTSP_4:33;

assume x + y in the carrier of W2 ; :: thesis: contradiction

then (x + y) - y in the carrier of W2 by A10, VECTSP_4:3;

then x + (y - y) in the carrier of W2 by RLVECT_1:def 3;

then x + (0. M) in the carrier of W2 by VECTSP_1:19;

hence contradiction by A8, RLVECT_1:4; :: thesis: verum

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

( x in the carrier of W & y in the carrier of W )
by A1, XBOOLE_0:def 3;reconsider A2 = the carrier of W1 as Subset of M by VECTSP_4:def 2;

A12: A2 is linearly-closed by VECTSP_4:33;

assume x + y in the carrier of W1 ; :: thesis: contradiction

then (y + x) - x in the carrier of W1 by A12, VECTSP_4:3;

then y + (x - x) in the carrier of W1 by RLVECT_1:def 3;

then y + (0. M) in the carrier of W1 by VECTSP_1:19;

hence contradiction by A5, RLVECT_1:4; :: thesis: verum

end;A12: A2 is linearly-closed by VECTSP_4:33;

assume x + y in the carrier of W1 ; :: thesis: contradiction

then (y + x) - x in the carrier of W1 by A12, VECTSP_4:3;

then y + (x - x) in the carrier of W1 by RLVECT_1:def 3;

then y + (0. M) in the carrier of W1 by VECTSP_1:19;

hence contradiction by A5, RLVECT_1:4; :: thesis: verum

then x + y in the carrier of W by A6;

hence contradiction by A1, A11, A9, XBOOLE_0:def 3; :: thesis: verum

A13: now :: thesis: ( W1 is Subspace of W2 & ( 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 )

assume
W1 is Subspace of W2
; :: 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 )

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 ( ( 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 ) ; :: thesis: verum

end;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 ( ( 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 ) ; :: thesis: verum

A14: now :: thesis: ( W2 is Subspace of W1 & ( 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 )

assume
( 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 W2assume
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 )

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 ( ( 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 ) ; :: thesis: verum

end;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 ( ( 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 ) ; :: thesis: verum

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