for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic