theorem :: GLIB_000:20

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