:: deftheorem Def27 defines real-weighted GLIB_003:def 27 :
for GSq being WGraphSeq holds
( GSq is real-weighted iff for x being Nat holds GSq . x is real-weighted );