for G1 being _finite non _trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v holds
( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() )