let X be non empty TopSpace; :: thesis: for x0, x1 being Point of X st x0,x1 are_connected holds
pi_1 (X,x0), pi_1 (X,x1) are_isomorphic
let x0, x1 be Point of X; :: thesis: ( x0,x1 are_connected implies pi_1 (X,x0), pi_1 (X,x1) are_isomorphic )
consider P being Path of x1,x0;
assume A1: x0,x1 are_connected ; :: thesis: pi_1 (X,x0), pi_1 (X,x1) are_isomorphic
then reconsider h = pi_1-iso P as Homomorphism of (pi_1 (X,x0)),(pi_1 (X,x1)) by Th51;
take h ; :: according to GROUP_6:def 15 :: thesis: h is bijective
thus h is bijective by A1, Th56; :: thesis: verum