theorem :: GLIB_003:37

for G being EGraph
for e1, e2, x being set st e1 <> e2 holds
(the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2