theorem Th4: :: FINTOPO5:4

for FT1, FT2 being non empty RelStr
for h being Function of FT1,FT2
for n being Nat
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )