x0,x1 are_connected by BORSUK_2:def 3;
hence pi_1-iso P is Homomorphism of pi_1 T,x1, pi_1 T,x0 by Th51; :: thesis: verum