:: deftheorem Def15 defines real-elabeled GLIB_003:def 15 :
for G being EGraph holds
( G is real-elabeled iff the_ELabel_of G is real-valued );