for T being non empty TopSpace st T is having_trivial_Fundamental_Group holds
for t being Point of T
for P, Q being Loop of t holds P,Q are_homotopic