let G1 be non locally-finite _Graph; :: thesis:
let V be finite Subset of (the_Vertices_of G1); :: thesis:
let G2 be removeVertices of G1,V; :: thesis:
assume A1: for v being Vertex of G1 st v in V holds
v .edgesInOut() is finite ; :: thesis:

per cases ) \ V is non empty Subset of (the_Vertices_of G1) or not (the_Vertices_of G1) \ V is non empty Subset of (the_Vertices_of G1) ) ;

suppose A2: (the_Vertices_of G1) \ V is non empty Subset of (the_Vertices_of G1) ; :: thesis:

consider v1 being Vertex of G1 such that
A3: v1 .edgesInOut() is infinite by Def5;
A4: the_Vertices_of G2 = (the_Vertices_of G1) \ V by A2, GLIB_000:def 37;
not v1 in V by A1, A3;
then reconsider v2 = v1 as Vertex of G2 by A4, XBOOLE_0:def 5;
not the_Vertices_of G1 c= V by A2, XBOOLE_1:37;
then V c< the_Vertices_of G1 by XBOOLE_0:def 8;
then A5: v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) by GLIBPRE0:44;
deffunc H₁( Vertex of G1) -> Element of bool (the_Edges_of G1) = $1 .edgesInOut() ;
set S = { H₁(v) where v is Vertex of G1 : v in V } ;
A6: V is finite ;
A7: { H₁(v) where v is Vertex of G1 : v in V } is finite from FRAENKEL:sch 21(A6);

let X be set ; :: thesis:
assume X in { H₁(v) where v is Vertex of G1 : v in V } ; :: thesis:
then consider v being Vertex of G1 such that
A8: ( X = H₁(v) & v in V ) ;
thus X is finite by A1, A8; :: thesis:

end;

then union { H₁(v) where v is Vertex of G1 : v in V } is finite by A7, FINSET_1:7;
then G1 .edgesInOut V is finite by GLIBPRE0:38;
hence not G2 is locally-finite by A3, A5; :: thesis:

end;

suppose (the_Vertices_of G1) \ V is not non empty Subset of (the_Vertices_of G1) ; :: thesis:

then G1 == G2 by GLIB_000:def 37;
hence not G2 is locally-finite by Th24; :: thesis:

end;

end;