let l be Loop of t; :: thesis: ( l is constant implies l is nullhomotopic )
assume l is constant ; :: thesis: l is nullhomotopic
then reconsider l = l as constant Loop of t ;
take l ; :: according to TOPALG_6:def 3 :: thesis: l,l are_homotopic
thus l,l are_homotopic by BORSUK_6:88; :: thesis: verum