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