for T being TopStruct holds id T is being_homeomorphism by RELAT_1:45;