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