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