:: deftheorem Def25 defines [ELabeled] GLIB_003:def 25 :
for GSq being GraphSeq holds
( GSq is [ELabeled] iff for x being Nat holds GSq . x is [ELabeled] );