:: deftheorem defines .labeledE() GLIB_003:def 20 :
for G being EGraph holds G .labeledE() = dom (the_ELabel_of G);