:: deftheorem Def64 defines Dsimple GLIB_000:def 81 :
for GSq being GraphSeq holds
( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple );