theorem :: GLIB_000:122

for G being _Graph st ex v being Vertex of G st v is endvertex holds
not G is _trivial