for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order())