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