id T is Homeomorphism of T ;
hence not the carrier of (HomeoGroup T) is empty by Def5; :: according to STRUCT_0:def 1 :: thesis: verum