let X be non empty TopSpace; 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; ( 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 that
A1:
A1,A2 are_weakly_separated
and
A2:
not A1 c= A2
and
A3:
not A2 c= A1
; 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;
A4:
A1 \ A2 <> {}
by A2, XBOOLE_1:37;
A5:
A2 \ A1 <> {}
by A3, XBOOLE_1:37;
A6:
A1 c= A1 \/ A2
by XBOOLE_1:7;
A7:
A2 c= A1 \/ A2
by XBOOLE_1:7;
consider C1, C2, C being Subset of X such that
A8:
C1 /\ (A1 \/ A2) c= A1
and
A9:
C2 /\ (A1 \/ A2) c= A2
and
A10:
C /\ (A1 \/ A2) c= A1 /\ A2
and
A11:
the carrier of X = (C1 \/ C2) \/ C
and
A12:
( C1 is closed & C2 is closed )
and
A13:
C is open
by A1, Th54;
A1 /\ A2 c= A1
by XBOOLE_1:17;
then
C /\ (A1 \/ A2) c= A1
by A10, XBOOLE_1:1;
then
(C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2)) c= A1
by A8, XBOOLE_1:8;
then
(C \/ C1) /\ (A1 \/ A2) c= A1
by XBOOLE_1:23;
then
A2 \ A1 c= (A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2))
by A7, XBOOLE_1:35;
then A14:
A2 \ A1 c= (A1 \/ A2) \ (C \/ C1)
by XBOOLE_1:47;
A1 /\ A2 c= A2
by XBOOLE_1:17;
then
C /\ (A1 \/ A2) c= A2
by A10, XBOOLE_1:1;
then
(C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) c= A2
by A9, XBOOLE_1:8;
then
(C2 \/ C) /\ (A1 \/ A2) c= A2
by XBOOLE_1:23;
then
A1 \ A2 c= (A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2))
by A6, XBOOLE_1:35;
then A15:
A1 \ A2 c= (A1 \/ A2) \ (C2 \/ C)
by XBOOLE_1:47;
A16:
A1 \/ A2 c= [#] X
;
then
A1 \/ A2 c= (C \/ C1) \/ C2
by A11, XBOOLE_1:4;
then
(A1 \/ A2) \ (C \/ C1) c= C2
by XBOOLE_1:43;
then reconsider D2 = C2 as non empty Subset of X by A14, A5, XBOOLE_1:1, XBOOLE_1:3;
A1 \/ A2 c= (C2 \/ C) \/ C1
by A11, A16, XBOOLE_1:4;
then
(A1 \/ A2) \ (C2 \/ C) c= C1
by XBOOLE_1:43;
then reconsider D1 = C1 as non empty Subset of X by A15, A4, XBOOLE_1:1, XBOOLE_1:3;
take
D1
; 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
; ( 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 ) ) )
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 A8, A9, A12; verum