:: deftheorem defines are_homeomorphic T_0TOPSP:def 1 :
for T, S being TopStruct holds
( T,S are_homeomorphic iff ex f being Function of T,S st f is being_homeomorphism );