theorem Th15: :: TOPALG_6:15
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