theorem Th20: :: GLIB_000:20

for G being non _trivial _Graph
for v being Vertex of G holds not (the_Vertices_of G) \ {v} is empty