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 ) ) ) ) ) )
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 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 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 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 :: 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 ) ) ) ) implies X1,X2 are_weakly_separated )
assume A5: ( 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 :: 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 open 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 closed 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 closed )
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 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 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 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
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 closed by Th11;
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 closed ) by A14, A13; :: thesis: verum
end;
end;
end;
end;
A15: ( C1 is open & C2 is open ) by Th16;
( 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, Th60;
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 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 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 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 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 ( 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
A17: C1 is open and
A18: C2 is open 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 closed ) ) by A2, A16, Th61;
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 Y2 being non empty strict open SubSpace of X such that
A21: C2 = the carrier of Y2 by A18, Th20;
consider Y1 being non empty strict open SubSpace of X such that
A22: C1 = the carrier of Y1 by A17, 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 :: thesis: ( X <> Y1 union Y2 implies ex Y being non empty closed 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 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
A23: A1 \/ A2 = (C1 \/ C2) \/ C and
A24: C c= A1 /\ A2 and
A25: C is closed by A1, A2, A20, A22, A21, 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
A26: C c= the carrier of (X1 meet X2) by A3, A24, Def4;
consider Y being non empty strict closed SubSpace of X such that
A27: C = the carrier of Y by A25, Th15;
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 closed 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 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;
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