let X be non empty TopSpace; :: thesis:
let A1, A2 be Subset of X; :: thesis:
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:

assume A1,A2 are_separated ; :: thesis:
then consider B1, B2 being Subset of X such that
A1: ( A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) and
A2: ( B1 is open & B2 is open ) by Th49;
take B1 ; :: thesis:
take B2 ; :: thesis:
thus ( B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 ) by A1, A2, Th54; :: thesis:

end;

given B1, B2 being Subset of X such that A3: B1,B2 are_weakly_separated and
A4: ( A1 c= B1 & A2 c= B2 ) and
A5: B1 /\ B2 misses A1 \/ A2 ; :: thesis:
A6: ( A1 /\ B2 c= A1 & A1 /\ B2 c= B1 /\ B2 & B1 /\ A2 c= A2 & B1 /\ A2 c= B1 /\ B2 ) by A4, XBOOLE_1:17, XBOOLE_1:26;
( B1 /\ B2 misses A1 & B1 /\ B2 misses A2 ) by A5, XBOOLE_1:7, XBOOLE_1:63;
then ( (B1 /\ B2) /\ A1 = {} & (B1 /\ B2) /\ A2 = {} ) by XBOOLE_0:def 7;
then A7: ( A1 /\ B2 = {} & B1 /\ A2 = {} ) by A6, XBOOLE_1:3, XBOOLE_1:19;
( A1 \ B2 c= B1 \ B2 & A2 \ B1 c= B2 \ B1 ) by A4, XBOOLE_1:33;
then A8: ( A1 \ (A1 /\ B2) c= B1 \ B2 & A2 \ (B1 /\ A2) c= B2 \ B1 ) by XBOOLE_1:47;
B1 \ B2,B2 \ B1 are_separated by A3, Def7;
hence A1,A2 are_separated by A7, A8, CONNSP_1:8; :: thesis: