for T being non empty having_trivial_Fundamental_Group TopSpace
for t being Point of T
for P1, P2 being Loop of t holds P1,P2 are_homotopic