theorem :: GLIB_003:46

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