theorem :: METRIZTS:1

for T1, T2 being TopSpace holds
( T1,T2 are_homeomorphic iff [#] T1, [#] T2 are_homeomorphic )