:: deftheorem Def63 defines simple GLIB_000:def 80 :
for GSq being GraphSeq holds
( GSq is simple iff for x being Nat holds GSq . x is simple );