:: deftheorem Def30 defines real-vlabeled GLIB_003:def 30 :
for GSq being VGraphSeq holds
( GSq is real-vlabeled iff for x being Nat holds GSq . x is real-vlabeled );