:: deftheorem defines being_homeomorphism TOPS_2:def 5 :
for S, T being TopStruct
for f being Function of S,T holds
( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) );