theorem :: GLIB_003:44

for G1, G2 being EGraph st the_ELabel_of G1 = the_ELabel_of G2 holds
G1 .labeledE() = G2 .labeledE() ;