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

per cases ( (the_Vertices_of G1) \ 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: not G2 is locally-finite

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 GLIB_000:166;
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);

now :: thesis: for X being set st X in { H₁(v) where v is Vertex of G1 : v in V } holds
X is finite

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

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 GLIB_000:160;
hence not G2 is locally-finite by A3, A5; :: thesis: verum

end;

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

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

end;

end;