x0,x1 are_connected by BORSUK_2:def 3;
hence ( pi_1-iso P is one-to-one & pi_1-iso P is onto ) by Th51, Th52; :: thesis: verum