for X being non empty TopSpace
for x0, x1 being Point of X st x0,x1 are_connected holds
pi_1 (X,x0), pi_1 (X,x1) are_isomorphic