let T be TopStruct ; :: thesis: id T is being_homeomorphism
thus ( dom (id T) = [#] T & rng (id T) = [#] T ) by RELAT_1:45; :: according to TOPS_2:def 5 :: thesis: ( id T is one-to-one & id T is continuous & (id T) /" is continuous )
thus ( id T is one-to-one & id T is continuous & (id T) /" is continuous ) ; :: thesis: verum