set G0 = the non vertex-finite _Graph;
take G = the addAdjVertexAll of the non vertex-finite _Graph, the_Vertices_of the non vertex-finite _Graph, the_Vertices_of the non vertex-finite _Graph; :: thesis: not G is locally-finite
( the_Vertices_of the non vertex-finite _Graph is infinite & the_Vertices_of the non vertex-finite _Graph c= the_Vertices_of the non vertex-finite _Graph ) ;
hence not G is locally-finite ; :: thesis: verum