theorem :: GLIB_003:33

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