:: deftheorem Def16 defines real-vlabeled GLIB_003:def 16 :
for G being VGraph holds
( G is real-vlabeled iff the_VLabel_of G is real-valued );