theorem Th116: :: GLIB_000:116

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