theorem Th16: :: GLIB_008:16

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