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 that
A1: A1,A2 are_weakly_separated and
A2: not A1 c= A2 and
A3: 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;
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 ; :: 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 :: thesis: ( not A1 \/ A2 c= C1 \/ C2 implies 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 ) )
assume A17: 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 A11, A17;
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 A10, A11, A13; :: 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 A8, A9, A12; :: thesis: verum