for G1 being _Graph
for E being set
for G2 being removeEdges of G1,E holds G1 .order() = G2 .order() by Th53;