let T be non empty pathwise_connected TopSpace; :: thesis: for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic
let y0, y1 be Point of T; :: thesis: pi_1 (T,y0), pi_1 (T,y1) are_isomorphic
set R = the Path of y1,y0;
take pi_1-iso the Path of y1,y0 ; :: according to GROUP_6:def 11 :: thesis: pi_1-iso the Path of y1,y0 is bijective
thus pi_1-iso the Path of y1,y0 is bijective ; :: thesis: verum