let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X = X1 union X2 & X1 meets X2 implies ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ) )
assume A1: X = X1 union X2 ; :: thesis: ( not X1 meets X2 or ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ) )
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
A2: A1 \/ A2 = the carrier of X by A1, Def2;
assume A3: X1 meets X2 ; :: thesis: ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )

A4: now

assume X1,X2 are_weakly_separated ; :: thesis: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) )
then A5: A1,A2 are_weakly_separated by Def9;

now

assume ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: thesis: ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) )
then ( not A1 c= A2 & not A2 c= A1 ) by Th4;
then consider C1, C2 being non empty Subset of X such that
A6: ( C1 is open & C2 is open & C1 c= A1 & C2 c= A2 ) and
A7: ( A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed ) ) by A2, A5, Th66;
thus ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) :: thesis: verum

proof

consider Y1 being non empty strict open SubSpace of X such that
A8: C1 = the carrier of Y1 by A6, Th20;
consider Y2 being non empty strict open SubSpace of X such that
A9: C2 = the carrier of Y2 by A6, Th20;
take Y1 ; :: thesis: ex Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) )
take Y2 ; :: thesis: ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) )

now

assume X <> Y1 union Y2 ; :: thesis: ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 )
then consider C being non empty Subset of X such that
A10: ( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed ) by A1, A2, A7, A8, A9, Def2;
thus ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) :: thesis: verum

proof

consider Y being non empty strict closed SubSpace of X such that
A11: C = the carrier of Y by A10, Th15;
take Y ; :: thesis: ( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 )
A12: the carrier of X = the carrier of (Y1 union Y2) \/ C by A2, A8, A9, A10, Def2
.= the carrier of ((Y1 union Y2) union Y) by A11, Def2 ;
C c= the carrier of (X1 meet X2) by A3, A10, Def5;
hence ( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) by A1, A11, A12, Th4, Th5; :: thesis: verum

end;

end;

hence ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) by A6, A8, A9, Th4; :: thesis: verum

end;

end;

hence ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ; :: thesis: verum

end;

now

assume A13: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ; :: thesis: X1,X2 are_weakly_separated

now

assume ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: thesis: X1,X2 are_weakly_separated
then consider Y1, Y2 being non empty open SubSpace of X such that
A14: ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 ) and
A15: ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) by A13;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
A16: ( C1 is open & C2 is open ) by Th16;
A17: ( C1 c= A1 & C2 c= A2 ) by A14, Th4;

now

per cases ( A1 \/ A2 = C1 \/ C2 or A1 \/ A2 <> C1 \/ C2 ) ;

suppose A18: A1 \/ A2 = C1 \/ C2 ; :: thesis: ex C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed )

thus ex C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed ) :: thesis: verum

proof

take {} X ; :: thesis: ( A1 \/ A2 = (C1 \/ C2) \/ ({} X) & {} X c= A1 /\ A2 & {} X is closed )
thus ( A1 \/ A2 = (C1 \/ C2) \/ ({} X) & {} X c= A1 /\ A2 & {} X is closed ) by A18, XBOOLE_1:2; :: thesis: verum

end;

end;

suppose A19: A1 \/ A2 <> C1 \/ C2 ; :: thesis: ex C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed )

thus ex C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed ) :: thesis: verum

proof

consider Y being non empty closed SubSpace of X such that
A20: ( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) by A2, A15, A19, Def2;
reconsider C = the carrier of Y as Subset of X by Th1;
A21: C is closed by Th11;
A1 /\ A2 = the carrier of (X1 meet X2) by A3, Def5;
then A22: C c= A1 /\ A2 by A20, Th4;
A1 \/ A2 = the carrier of (Y1 union Y2) \/ C by A2, A20, Def2
.= (C1 \/ C2) \/ C by Def2 ;
hence ex C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed ) by A21, A22; :: thesis: verum

end;

end;

end;

end;

then for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated by A2, A16, A17, Th65;
hence X1,X2 are_weakly_separated by Def9; :: thesis: verum

end;

hence X1,X2 are_weakly_separated by Th86; :: thesis: verum

end;

hence ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ) by A4; :: thesis: verum