for G2 being _finite _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1