let T be TopSpace; :: thesis: for A, B being Subset of
for C, D being Subset of st A = C & B = D holds
( A,B are_separated iff C,D are_separated )
let A, B be Subset of ; :: thesis: for C, D being Subset of st A = C & B = D holds
( A,B are_separated iff C,D are_separated )
let C, D be Subset of ; :: thesis: ( A = C & B = D implies ( A,B are_separated iff C,D are_separated ) )
assume A1: ( A = C & B = D ) ; :: thesis: ( A,B are_separated iff C,D are_separated )
then A2: ( Cl A = Cl C & Cl B = Cl D ) by TOPS_3:80;

hereby :: thesis: ( C,D are_separated implies A,B are_separated )

assume A,B are_separated ; :: thesis: C,D are_separated
then ( Cl A misses B & A misses Cl B ) by CONNSP_1:def 1;
hence C,D are_separated by A1, A2, CONNSP_1:def 1; :: thesis: verum

end;

assume C,D are_separated ; :: thesis: A,B are_separated
then ( Cl C misses D & C misses Cl D ) by CONNSP_1:def 1;
hence A,B are_separated by A1, A2, CONNSP_1:def 1; :: thesis: verum