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 ) ) ) ) ) )
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 ) ) ) ) ) )
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 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

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 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 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
A6: ( C1 is closed & C2 is closed & 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 open ) ) by A2, A5, Th62;
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 Y1 being non empty strict closed SubSpace of X such that
A8: C1 = the carrier of Y1 by A6, Th15;
consider Y2 being non empty strict closed SubSpace of X such that
A9: C2 = the carrier of Y2 by A6, 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

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
A10: ( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open ) by A1, A2, A7, A8, A9, 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

consider Y being non empty strict open SubSpace of X such that
A11: C = the carrier of Y by A10, Th20;
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 open 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 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;

now

assume A13: ( 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

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
A14: ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 ) and
A15: ( 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 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 closed & C2 is closed ) by Th11;
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 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 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 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
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 open by Th16;
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 open ) 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, Th61;
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 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