theorem Th45: :: GLIB_003:45
for G being EGraph
for e, x being set st e in the_Edges_of G holds
(G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e}