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