let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 holds
ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( 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 ) ) )
let A1, A2 be Subset of X; :: thesis: ( A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( 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 ) ) ) )
assume A1: A1 \/ A2 = the carrier of X ; :: thesis: ( not A1,A2 are_weakly_separated or A1 c= A2 or A2 c= A1 or ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( 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 ) ) ) )
assume ( A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 ) ; :: thesis: ex C1, C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( 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 ) ) )
then consider C1, C2 being non empty Subset of X such that
A2: ( C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 ) and
A3: ( A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) ) by Th55;
take C1 ; :: thesis: ex C2 being non empty Subset of X st
( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( 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 ) ) )
take C2 ; :: thesis: ( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( 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 ) ) )
now :: thesis: ( not A1 \/ A2 = C1 \/ C2 implies ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open ) )
assume not A1 \/ A2 = C1 \/ C2 ; :: thesis: ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open )
then consider C being non empty Subset of X such that
A4: ( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) by A1, A3, XBOOLE_0:def 10;
thus ex C being non empty Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open ) :: thesis: verum
proof
take C ; :: thesis: ( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open )
thus ( A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open ) by A1, A4, XBOOLE_1:28; :: thesis: verum
end;
end;
hence ( C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ( 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 A1, A2, XBOOLE_1:28; :: thesis: verum