theorem :: GLIB_000:25

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