for G being _finite connected _Graph holds G .order() <= (G .size()) + 1