:: deftheorem Def3 defines plain GLIBPRE0:def 3 :
for GSq being GraphSeq holds
( GSq is plain iff for n being Nat holds GSq . n is plain );