let T be TopSpace; :: thesis: for A, B being Subset of T
for C, D being Subset of TopStruct(# the carrier of T, the topology of T #) st A = C & B = D holds
( A,B are_separated iff C,D are_separated )
let A, B be Subset of T; :: thesis: for C, D being Subset of TopStruct(# the carrier of T, the topology of T #) st A = C & B = D holds
( A,B are_separated iff C,D are_separated )
let C, D be Subset of TopStruct(# the carrier of T, the topology of T #); :: 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