theorem :: GLIB_000:26

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