theorem Th32: :: GLIB_003:32

for G being EGraph
for e, x being set st e in the_Edges_of G holds
the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x)