theorem :: GLIB_000:55

for G1 being _finite _Graph
for E being Subset of (the_Edges_of G1)
for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size()