let G1 be _finite _Graph; :: thesis: for E being Subset of (the_Edges_of G1)
for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size()
let E be Subset of (the_Edges_of G1); :: thesis: for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size()
let G2 be removeEdges of G1,E; :: thesis: (G2 .size()) + (card E) = G1 .size()
A1: the_Edges_of G2 = (the_Edges_of G1) \ E by Th53;
then the_Edges_of G1 = (the_Edges_of G2) \/ E by XBOOLE_1:45;
hence (G2 .size()) + (card E) = G1 .size() by A1, CARD_2:40, XBOOLE_1:79; :: thesis: verum