A1: id T is being_homeomorphism by Th20;
then T,T are_homeomorphic by T_0TOPSP:def 1;
then reconsider f = id T as Homeomorphism of T,T by A1, Def3;
f is being_homeomorphism by Th20;
hence ex b₁ being Function of T,T st b₁ is being_homeomorphism ; :: thesis: verum