theorem :: GLIB_003:47

for G being _finite EGraph
for e, x being set st e in the_Edges_of G & not e in G .labeledE() holds
card ((G .labelEdge (e,x)) .labeledE()) = (card (G .labeledE())) + 1