theorem Th17: :: TOPALG_6:17

for T being non empty TopSpace st ( for t being Point of T
for f being Loop of t holds f is nullhomotopic ) holds
T is having_trivial_Fundamental_Group