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 )
assume A1: x0,x1 are_connected ; :: thesis: pi_1 X,x0, pi_1 X,x1 are_isomorphic
consider P being Path of x1,x0;
reconsider h = pi_1-iso P as Homomorphism of (pi_1 X,x0),(pi_1 X,x1) by A1, Th51;
take h ; :: according to GROUP_6:def 15 :: thesis: h is bijective
thus h is bijective by A1, Th56; :: thesis: verum