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