:: deftheorem defines nullhomotopic TOPALG_6:def 3 :
for T being non empty TopSpace
for t being Point of T
for l being Loop of t holds
( l is nullhomotopic iff ex c being constant Loop of t st l,c are_homotopic );