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;