theorem :: GLIB_000:25

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