theorem :: GLIB_003:48

for G being EGraph
for e1, e2, x being set st not e2 in G .labeledE() & e2 in (G .labelEdge (e1,x)) .labeledE() holds
( e1 = e2 & e1 in the_Edges_of G )