:: deftheorem Def58 defines loopless GLIB_000:def 75 :
for GSq being GraphSeq holds
( GSq is loopless iff for x being Nat holds GSq . x is loopless );