theorem :: GLIB_000:169

for G being _Graph holds
( G is _trivial iff the_Vertices_of G is trivial )