:: deftheorem Def4 defines loopfull GLIB_012:def 4 :
for GSq being GraphSeq holds
( GSq is loopfull iff for n being Nat holds GSq . n is loopfull );