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