let X be non empty TopSpace; 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; ( 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 ) )
( 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
; 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; verum