theorem :: GLIB_000:21

for G being non _trivial _Graph ex v1, v2 being Vertex of G st v1 <> v2