:: deftheorem defines elabel-preserving GLIB_010:def 26 :
for G1, G2 being EGraph
for F being PGraphMapping of G1,G2 holds
( F is elabel-preserving iff (the_ELabel_of G2) * (F _E) = (the_ELabel_of G1) | (dom (F _E)) );