id T is being_homeomorphism by Th19;
hence T,T are_homeomorphic ; :: according to TOPGRP_1:def 3 :: thesis: id T is being_homeomorphism
thus id T is being_homeomorphism by Th19; :: thesis: verum