:: deftheorem Def28 defines nonnegative-weighted GLIB_003:def 28 :
for GSq being WGraphSeq holds
( GSq is nonnegative-weighted iff for x being Nat holds GSq . x is nonnegative-weighted );