let G1 be addAdjVertexAll of G,v,V; :: thesis: G1 is locally-finite
per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;
suppose ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G1 is locally-finite
hence G1 is locally-finite by Th29; :: thesis: verum
end;
suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G1 is locally-finite
then G1 == G by GLIB_007:def 4;
hence G1 is locally-finite by Th24; :: thesis: verum
end;
end;