theorem Th10: :: GLIB_008:10

for G being _Graph st ex v1, v2 being Vertex of G st v1 <> v2 holds
not G is trivial