let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) )
let A1, A2 be Subset of X; :: thesis: ( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) )
set B1 = A1 \ A2;
set B2 = A2 \ A1;
A1: (A1 \/ A2) ` misses A1 \/ A2 by XBOOLE_1:79;
thus ( A1,A2 are_weakly_separated implies ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) ) :: thesis: ( ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) implies A1,A2 are_weakly_separated )
proof
assume A1,A2 are_weakly_separated ; :: thesis: ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
then A1 \ A2,A2 \ A1 are_separated ;
then consider C1, C2 being Subset of X such that
A2: ( A1 \ A2 c= C1 & A2 \ A1 c= C2 ) and
A3: C1 misses A2 \ A1 and
A4: C2 misses A1 \ A2 and
A5: ( C1 is open & C2 is open ) by Th44;
C1 /\ (A2 \ A1) = {} by A3, XBOOLE_0:def 7;
then (C1 /\ A2) \ (C1 /\ A1) = {} by XBOOLE_1:50;
then A6: C1 /\ A2 c= C1 /\ A1 by XBOOLE_1:37;
take C1 ; :: thesis: ex C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
take C2 ; :: thesis: ex C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
take C = (C1 \/ C2) ` ; :: thesis: ( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed )
(A1 \ A2) \/ (A2 \ A1) c= C1 \/ C2 by A2, XBOOLE_1:13;
then C c= ((A1 \ A2) \/ (A2 \ A1)) ` by SUBSET_1:12;
then C c= (A1 \+\ A2) ` by XBOOLE_0:def 6;
then C c= ((A1 \/ A2) \ (A1 /\ A2)) ` by XBOOLE_1:101;
then C c= ((A1 \/ A2) `) \/ (A1 /\ A2) by SUBSET_1:14;
then C /\ (A1 \/ A2) c= (((A1 \/ A2) `) \/ (A1 /\ A2)) /\ (A1 \/ A2) by XBOOLE_1:26;
then C /\ (A1 \/ A2) c= (((A1 \/ A2) `) /\ (A1 \/ A2)) \/ ((A1 /\ A2) /\ (A1 \/ A2)) by XBOOLE_1:23;
then A7: C /\ (A1 \/ A2) c= ({} X) \/ ((A1 /\ A2) /\ (A1 \/ A2)) by A1, XBOOLE_0:def 7;
C2 /\ (A1 \ A2) = {} by A4, XBOOLE_0:def 7;
then (C2 /\ A1) \ (C2 /\ A2) = {} by XBOOLE_1:50;
then A8: C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
C2 /\ (A1 \/ A2) = (C2 /\ A1) \/ (C2 /\ A2) by XBOOLE_1:23;
then A9: C2 /\ (A1 \/ A2) = C2 /\ A2 by A8, XBOOLE_1:12;
C1 /\ (A1 \/ A2) = (C1 /\ A1) \/ (C1 /\ A2) by XBOOLE_1:23;
then A10: C1 /\ (A1 \/ A2) = C1 /\ A1 by A6, XBOOLE_1:12;
( [#] X = (C `) \/ C & (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 ) by PRE_TOPC:2, XBOOLE_1:17;
hence ( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) by A5, A10, A9, A7, XBOOLE_1:1, XBOOLE_1:17; :: thesis: verum
end;
given C1, C2, C being Subset of X such that A11: C1 /\ (A1 \/ A2) c= A1 and
A12: C2 /\ (A1 \/ A2) c= A2 and
A13: C /\ (A1 \/ A2) c= A1 /\ A2 and
A14: the carrier of X = (C1 \/ C2) \/ C and
A15: ( C1 is open & C2 is open ) and
C is closed ; :: thesis: A1,A2 are_weakly_separated
ex C1, C2 being Subset of X st
( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is open & C2 is open )
proof
(C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A11, A12, XBOOLE_1:27;
then (C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then (C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {} by XBOOLE_1:37;
then (C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {} by XBOOLE_1:49;
then A16: (C1 /\ C2) /\ ((A1 \ A2) \/ (A2 \ A1)) = {} by XBOOLE_1:55;
A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A2 by A13, XBOOLE_1:1;
then (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) c= A2 by A12, XBOOLE_1:8;
then A17: (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 \ A2 c= (A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2)) by A17, XBOOLE_1:35;
then A18: A1 \ A2 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A1 /\ A2 c= A1 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 by A13, XBOOLE_1:1;
then (C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2)) c= A1 by A11, XBOOLE_1:8;
then A19: (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then A2 \ A1 c= (A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2)) by A19, XBOOLE_1:35;
then A20: A2 \ A1 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
take C1 ; :: thesis: ex C2 being Subset of X st
( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is open & C2 is open )
take C2 ; :: thesis: ( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is open & C2 is open )
A21: A1 \/ A2 c= [#] X ;
then A1 \/ A2 c= (C2 \/ C) \/ C1 by A14, XBOOLE_1:4;
then A22: (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
A1 \/ A2 c= (C \/ C1) \/ C2 by A14, A21, XBOOLE_1:4;
then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
hence ( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is open & C2 is open ) by A15, A20, A18, A22, A16, XBOOLE_0:def 7, XBOOLE_1:1; :: thesis: verum
end;
then A1 \ A2,A2 \ A1 are_separated by Th45;
hence A1,A2 are_weakly_separated ; :: thesis: verum