card (the_Vertices_of G) = 1 by Def21;
hence the_Vertices_of G is finite ; :: thesis: verum