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