:: deftheorem defines being_homeomorphism FINTOPO5:def 1 :
for FT1, FT2 being RelStr
for h being Function of FT1,FT2 holds
( h is being_homeomorphism iff ( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) ) );