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 that
A1: B1 = A1 and
A2: B2 = A2 ; :: thesis: ( A1,A2 are_separated iff B1,B2 are_separated )
A3: Cl B2 = (Cl A2) /\ ([#] X0) by ;
A4: Cl B1 = (Cl A1) /\ ([#] X0) by ;
thus ( A1,A2 are_separated implies B1,B2 are_separated ) :: thesis: ( B1,B2 are_separated implies A1,A2 are_separated )
proof end;
thus ( B1,B2 are_separated implies A1,A2 are_separated ) :: thesis: verum
proof
assume A7: B1,B2 are_separated ; :: thesis: A1,A2 are_separated
then (Cl A1) /\ ([#] X0) misses A2 by ;
then ((Cl A1) /\ ([#] X0)) /\ A2 = {} ;
then A8: ((Cl A1) /\ A2) /\ ([#] X0) = {} by XBOOLE_1:16;
A1 misses (Cl A2) /\ ([#] X0) by ;
then A1 /\ ((Cl A2) /\ ([#] X0)) = {} ;
then A9: (A1 /\ (Cl A2)) /\ ([#] X0) = {} by XBOOLE_1:16;
A1 /\ (Cl A2) c= A1 by XBOOLE_1:17;
then A1 /\ (Cl A2) = {} by ;
then A10: A1 misses Cl A2 ;
(Cl A1) /\ A2 c= A2 by XBOOLE_1:17;
then (Cl A1) /\ A2 = {} by ;
then Cl A1 misses A2 ;
hence A1,A2 are_separated by ; :: thesis: verum
end;