theorem :: GLIBPRE1:18

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