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