theorem :: GLIB_000:26

for G being finite _Graph holds
( G .order() = 1 iff G is trivial ) ;