:: deftheorem Def3 defines elabel-distinct GLIB_010:def 3 :
for G being EGraph holds
( G is elabel-distinct iff the_ELabel_of G is one-to-one );