for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds G1 .minDegree() c= (G2 .minDegree()) +` 2