let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X holds
( A1,A2 are_separated iff ex B1, B2 being Subset of X st
( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) )
let A1, A2 be Subset of X; :: thesis: ( A1,A2 are_separated iff ex B1, B2 being Subset of X st
( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) )
thus ( A1,A2 are_separated implies ex B1, B2 being Subset of X st
( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) ) :: thesis: ( ex B1, B2 being Subset of X st
( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) implies A1,A2 are_separated ) given B1, B2 being Subset of X such that A2: B1,B2 are_weakly_separated and
A3: A1 c= B1 and
A4: A2 c= B2 and
A5: B1 /\ B2 misses A1 \/ A2 ; :: thesis: A1,A2 are_separated
B1 /\ B2 misses A1 by A5, XBOOLE_1:7, XBOOLE_1:63;
then A6: (B1 /\ B2) /\ A1 = {} by XBOOLE_0:def 7;
B1 /\ B2 misses A2 by A5, XBOOLE_1:7, XBOOLE_1:63;
then A7: (B1 /\ B2) /\ A2 = {} by XBOOLE_0:def 7;
( B1 /\ A2 c= A2 & B1 /\ A2 c= B1 /\ B2 ) by A4, XBOOLE_1:17, XBOOLE_1:26;
then A8: B1 /\ A2 = {} by A7, XBOOLE_1:3, XBOOLE_1:19;
A2 \ B1 c= B2 \ B1 by A4, XBOOLE_1:33;
then A9: A2 \ (B1 /\ A2) c= B2 \ B1 by XBOOLE_1:47;
( A1 /\ B2 c= A1 & A1 /\ B2 c= B1 /\ B2 ) by A3, XBOOLE_1:17, XBOOLE_1:26;
then A10: A1 /\ B2 = {} by A6, XBOOLE_1:3, XBOOLE_1:19;
A1 \ B2 c= B1 \ B2 by A3, XBOOLE_1:33;
then A11: A1 \ (A1 /\ B2) c= B1 \ B2 by XBOOLE_1:47;
B1 \ B2,B2 \ B1 are_separated by A2;
hence A1,A2 are_separated by A10, A8, A11, A9, CONNSP_1:7; :: thesis: verum