:: deftheorem Def26 defines [VLabeled] GLIB_003:def 26 :
for GSq being GraphSeq holds
( GSq is [VLabeled] iff for x being Nat holds GSq . x is [VLabeled] );