:: deftheorem Def29 defines real-elabeled GLIB_003:def 29 :
for GSq being EGraphSeq holds
( GSq is real-elabeled iff for x being Nat holds GSq . x is real-elabeled );