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 closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open 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 closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ) )
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
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 closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ) )
then A2: A1 \/ A2 = the carrier of X by 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 closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )

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

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

now :: thesis: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 implies X1,X2 are_weakly_separated )

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 closed SubSpace of X such that
A6: ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 ) and
A7: ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) by A5;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;

A8: now :: thesis: ex C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open )

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

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

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

proof

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

end;

end;

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

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

proof

consider Y being non empty open SubSpace of X such that
A11: X = (Y1 union Y2) union Y and
A12: Y is SubSpace of X1 meet X2 by A2, A7, A10, Def2;
reconsider C = the carrier of Y as Subset of X by Th1;
A1 /\ A2 = the carrier of (X1 meet X2) by A3, Def4;
then A13: C c= A1 /\ A2 by A12, Th4;
A14: C is open by Th16;
A1 \/ A2 = the carrier of (Y1 union Y2) \/ C by A2, A11, 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 open ) by A14, A13; :: thesis: verum

end;

end;

end;

end;

A15: ( C1 is closed & C2 is closed ) by Th11;
( C1 c= A1 & C2 c= A2 ) by A6, Th4;
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, A15, A8, Th56;
hence X1,X2 are_weakly_separated ; :: thesis: verum

end;

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

end;

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

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 closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) )
then A16: A1,A2 are_weakly_separated ;

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

assume ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: thesis: ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open 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
A17: C1 is closed and
A18: C2 is closed and
A19: ( C1 c= A1 & C2 c= A2 ) and
A20: ( 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 open ) ) by A2, A16, Th57;
thus ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) :: thesis: verum

proof

consider Y2 being non empty strict closed SubSpace of X such that
A21: C2 = the carrier of Y2 by A18, Th15;
consider Y1 being non empty strict closed SubSpace of X such that
A22: C1 = the carrier of Y1 by A17, Th15;
take Y1 ; :: thesis: ex Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open 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 open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) )

now :: thesis: ( X <> Y1 union Y2 implies ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) )

assume X <> Y1 union Y2 ; :: thesis: ex Y being non empty open 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
A23: A1 \/ A2 = (C1 \/ C2) \/ C and
A24: C c= A1 /\ A2 and
A25: C is open by A1, A2, A20, A22, A21, Def2;
thus ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) :: thesis: verum

proof

A26: C c= the carrier of (X1 meet X2) by A3, A24, Def4;
consider Y being non empty strict open SubSpace of X such that
A27: C = the carrier of Y by A25, Th20;
take Y ; :: thesis: ( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 )
the carrier of X = the carrier of (Y1 union Y2) \/ C by A2, A22, A21, A23, Def2
.= the carrier of ((Y1 union Y2) union Y) by A27, Def2 ;
hence ( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) by A1, A27, A26, 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 open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) by A19, A22, A21, Th4; :: thesis: verum

end;

end;

hence ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ; :: 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 closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ) by A4; :: thesis: verum