let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let A1, A2 be Subset of X; :: thesis: for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let X0 be non empty SubSpace of X; :: thesis: for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let B1, B2 be Subset of X0; :: thesis: ( B1 = A1 & B2 = A2 implies ( A1,A2 are_separated iff B1,B2 are_separated ) )
assume A1: ( B1 = A1 & B2 = A2 ) ; :: thesis: ( A1,A2 are_separated iff B1,B2 are_separated )
then A2: ( Cl B1 = (Cl A1) /\ ([#] X0) & Cl B2 = (Cl A2) /\ ([#] X0) ) by PRE_TOPC:47;
thus ( A1,A2 are_separated implies B1,B2 are_separated ) :: thesis: ( B1,B2 are_separated implies A1,A2 are_separated )

proof

assume A1,A2 are_separated ; :: thesis: B1,B2 are_separated
then ( Cl A1 misses A2 & A1 misses Cl A2 ) by CONNSP_1:def 1;
then ( (Cl A1) /\ A2 = {} & A1 /\ (Cl A2) = {} ) by XBOOLE_0:def 7;
then ( (Cl B1) /\ B2 = {} /\ ([#] X0) & B1 /\ (Cl B2) = {} /\ ([#] X0) ) by A1, A2, XBOOLE_1:16;
then ( Cl B1 misses B2 & B1 misses Cl B2 ) by XBOOLE_0:def 7;
hence B1,B2 are_separated by CONNSP_1:def 1; :: thesis: verum

end;

thus ( B1,B2 are_separated implies A1,A2 are_separated ) :: thesis: verum

proof

assume B1,B2 are_separated ; :: thesis: A1,A2 are_separated
then ( (Cl A1) /\ ([#] X0) misses A2 & A1 misses (Cl A2) /\ ([#] X0) ) by A1, A2, CONNSP_1:def 1;
then ( ((Cl A1) /\ ([#] X0)) /\ A2 = {} & A1 /\ ((Cl A2) /\ ([#] X0)) = {} ) by XBOOLE_0:def 7;
then A3: ( ((Cl A1) /\ A2) /\ ([#] X0) = {} & (A1 /\ (Cl A2)) /\ ([#] X0) = {} ) by XBOOLE_1:16;
( (Cl A1) /\ A2 c= A2 & A1 /\ (Cl A2) c= A1 & A2 c= [#] X0 & A1 c= [#] X0 ) by A1, XBOOLE_1:17;
then ( (Cl A1) /\ A2 = {} & A1 /\ (Cl A2) = {} ) by A3, XBOOLE_1:1, XBOOLE_1:28;
then ( Cl A1 misses A2 & A1 misses Cl A2 ) by XBOOLE_0:def 7;
hence A1,A2 are_separated by CONNSP_1:def 1; :: thesis: verum

end;