theorem Th5: :: TOPALG_5:5

for S, T being TopSpace
for A, B being Subset of T
for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds
C,D are_separated by TOPS_3:80;