:: deftheorem Def57 defines _finite GLIB_000:def 74 :
for GSq being GraphSeq holds
( GSq is _finite iff for x being Nat holds GSq . x is _finite );