:: deftheorem Def60 defines non-trivial GLIB_000:def 77 :
for GSq being GraphSeq holds
( GSq is non-trivial iff for x being Nat holds not GSq . x is _trivial );