thus id T is being_homeomorphism by Th19; :: according to TOPGRP_1:def 4 :: thesis: verum