let f be Homeomorphism of T; :: thesis: f is Homeomorphism of T,T
A1: f is being_homeomorphism by Def4;
then T,T are_homeomorphic by T_0TOPSP:def 1;
hence f is Homeomorphism of T,T by A1, Def3; :: thesis: verum