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 )
set P = the 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 the Path of x1,x0 as Homomorphism of (pi_1 (X,x0)),(pi_1 (X,x1)) by Th50;
take h ; :: according to GROUP_6:def 11 :: thesis: h is bijective
thus h is bijective by A1, Th55; :: thesis: verum