ex v being Vertex of G st the_Vertices_of G = {v} by GLIB_000:22;
hence the_Vertices_of G is trivial ; :: thesis: verum