let G1 be addVertices of G,V; :: thesis: G1 is locally-finite
let v be Vertex of G1; :: according to GLIB_013:def 5 :: thesis: v .edgesInOut() is finite
the_Vertices_of G1 = (the_Vertices_of G) \/ V by GLIB_006:def 10;

per cases then ( v in the_Vertices_of G or ( v in V & not v in the_Vertices_of G ) ) by XBOOLE_0:def 3;

suppose v in the_Vertices_of G ; :: thesis: v .edgesInOut() is finite

then reconsider v0 = v as Vertex of G ;
v0 .edgesInOut() is finite ;
hence v .edgesInOut() is finite by GLIBPRE0:45; :: thesis: verum

end;

suppose ( v in V & not v in the_Vertices_of G ) ; :: thesis: v .edgesInOut() is finite

then v in V \ (the_Vertices_of G) by XBOOLE_0:def 5;
hence v .edgesInOut() is finite by GLIB_006:88, GLIB_000:def 49; :: thesis: verum

end;

end;