theorem Th6: :: TOPALG_3:6
for T being TopSpace
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 ) by TOPS_3:80;