let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X st 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 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( 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 ) ) )
let A1, A2 be Subset of X; :: thesis: ( 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 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( 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 ) ) ) )
assume A1: ( 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 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( 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 ) ) )
set B1 = A1 \ A2;
set B2 = A2 \ A1;
consider C1, C2, C being Subset of X such that
A2: ( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 ) and
A3: the carrier of X = (C1 \/ C2) \/ C and
A4: ( C1 is closed & C2 is closed & C is open ) by A1, Th59;
( A1 /\ A2 c= A1 & A1 /\ A2 c= A2 ) by XBOOLE_1:17;
then ( C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 ) by A2, XBOOLE_1:1;
then ( (C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) c= A2 ) by A2, XBOOLE_1:8;
then ( (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 & A1 c= A1 \/ A2 & A2 c= A1 \/ A2 ) by XBOOLE_1:7, XBOOLE_1:23;
then ( A2 \ A1 c= (A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2)) & A1 \ A2 c= (A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2)) ) by XBOOLE_1:35;
then A5: ( A2 \ A1 c= (A1 \/ A2) \ (C \/ C1) & A1 \ A2 c= (A1 \/ A2) \ (C2 \/ C) ) by XBOOLE_1:47;
( A1 \/ A2 c= [#] X & [#] X = the carrier of X ) ;
then ( A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/ C1 ) by A3, XBOOLE_1:4;
then ( (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/ C) c= C1 ) by XBOOLE_1:43;
then A6: ( A2 \ A1 c= C2 & A1 \ A2 c= C1 & A1 \ A2 <> {} & A2 \ A1 <> {} ) by A1, A5, XBOOLE_1:1, XBOOLE_1:37;
then reconsider D1 = C1 as non empty Subset of X by XBOOLE_1:3;
reconsider D2 = C2 as non empty Subset of X by A6, XBOOLE_1:3;
take D1 ; :: thesis: ex C2 being non empty Subset of X st
( D1 is closed & C2 is closed & D1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & ( A1 \/ A2 c= D1 \/ C2 or ex C being non empty Subset of X st
( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (D1 \/ C2) \/ C ) ) )
take D2 ; :: thesis: ( D1 is closed & D2 is closed & D1 /\ (A1 \/ A2) c= A1 & D2 /\ (A1 \/ A2) c= A2 & ( A1 \/ A2 c= D1 \/ D2 or ex C being non empty Subset of X st
( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (D1 \/ D2) \/ C ) ) )

now

assume A7: not A1 \/ A2 c= C1 \/ C2 ; :: thesis: ex C being non empty Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is open )
thus ex C being non empty Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is open ) :: thesis: verum

proof

reconsider C0 = C as non empty Subset of X by A3, A7;
take C0 ; :: thesis: ( the carrier of X = (C1 \/ C2) \/ C0 & C0 /\ (A1 \/ A2) c= A1 /\ A2 & C0 is open )
thus ( the carrier of X = (C1 \/ C2) \/ C0 & C0 /\ (A1 \/ A2) c= A1 /\ A2 & C0 is open ) by A2, A3, A4; :: thesis: verum

end;

end;

hence ( D1 is closed & D2 is closed & D1 /\ (A1 \/ A2) c= A1 & D2 /\ (A1 \/ A2) c= A2 & ( A1 \/ A2 c= D1 \/ D2 or ex C being non empty Subset of X st
( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (D1 \/ D2) \/ C ) ) ) by A2, A4; :: thesis: verum