for G being _finite _Graph holds G .order() >= 1