:: deftheorem Def13 defines real-weighted GLIB_003:def 13 :
for G being WGraph holds
( G is real-weighted iff the_Weight_of G is real-valued );