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 Th52, Th53; :: thesis: verum