:: deftheorem Def19 defines _trivial GLIB_000:def 19 :
for G being _Graph holds
( G is _trivial iff card (the_Vertices_of G) = 1 );