let X be 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 closed & C2 is closed & C is open ) )
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 closed & C2 is closed & C is open ) )
set B1 = A1 \ A2;
set B2 = A2 \ A1;
A1: ( (A1 \/ A2) ` misses A1 \/ A2 & ((A1 \ A2) \/ (A2 \ A1)) ` misses (A1 \ A2) \/ (A2 \ A1) ) 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 closed & C2 is closed & C is open ) ) :: 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 closed & C2 is closed & C is open ) 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 closed & C2 is closed & C is open )
then A1 \ A2,A2 \ A1 are_separated by Def7;
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 & C2 misses A1 \ A2 ) and
A4: ( C1 is closed & C2 is closed ) by Th46;
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 closed & C2 is closed & C is open )
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 closed & C2 is closed & C is open )
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 closed & C2 is closed & C is open )
A5: C1 \/ C2 is closed by A4, TOPS_1:36;
A6: [#] X = C \/ (C ` ) by PRE_TOPC:18;
( C1 /\ (A2 \ A1) = {} & C2 /\ (A1 \ A2) = {} ) by A3, XBOOLE_0:def 7;
then ( (C1 /\ A2) \ (C1 /\ A1) = {} & (C2 /\ A1) \ (C2 /\ A2) = {} ) by XBOOLE_1:50;
then A7: ( C1 /\ A2 c= C1 /\ A1 & C2 /\ A1 c= C2 /\ A2 ) by XBOOLE_1:37;
( C1 /\ (A1 \/ A2) = (C1 /\ A1) \/ (C1 /\ A2) & C2 /\ (A1 \/ A2) = (C2 /\ A1) \/ (C2 /\ A2) ) by XBOOLE_1:23;
then A8: ( C1 /\ (A1 \/ A2) = C1 /\ A1 & C2 /\ (A1 \/ A2) = C2 /\ A2 ) by A7, XBOOLE_1:12;
(A1 \ A2) \/ (A2 \ A1) c= C1 \/ C2 by A2, XBOOLE_1:13;
then C c= ((A1 \ A2) \/ (A2 \ A1)) ` by SUBSET_1:31;
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:33;
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 C /\ (A1 \/ A2) c= ({} X) \/ ((A1 /\ A2) /\ (A1 \/ A2)) by A1, XBOOLE_0:def 7;
then ( C /\ (A1 \/ A2) c= (A1 /\ A2) /\ (A1 \/ A2) & (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 ) by 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 closed & C2 is closed & C is open ) by A4, A5, A6, A8, XBOOLE_1:1, XBOOLE_1:17; :: thesis: verum

end;

given C1, C2, C being Subset of X such that A9: ( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 ) and
A10: the carrier of X = (C1 \/ C2) \/ C and
A11: ( C1 is closed & C2 is closed & C is open ) ; :: 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 closed & C2 is closed )

proof

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 closed & C2 is closed )
take C2 ; :: thesis: ( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is closed & C2 is closed )
( A1 /\ A2 c= A1 & A1 /\ A2 c= A2 ) by XBOOLE_1:17;
then ( C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 ) by A9, XBOOLE_1:1;
then ( (C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) c= A2 ) by A9, 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 A12: ( 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 A10, XBOOLE_1:4;
then A13: ( (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/ C) c= C1 ) by XBOOLE_1:43;
(C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A9, 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 (C1 /\ C2) /\ ((A1 \ A2) \/ (A2 \ A1)) = {} by XBOOLE_1:55;
hence ( A1 \ A2 c= C1 & A2 \ A1 c= C2 & C1 /\ C2 misses (A1 \ A2) \/ (A2 \ A1) & C1 is closed & C2 is closed ) by A11, A12, A13, XBOOLE_0:def 7, XBOOLE_1:1; :: thesis: verum

end;

then A1 \ A2,A2 \ A1 are_separated by Th47;
hence A1,A2 are_weakly_separated by Def7; :: thesis: verum