let G2 be removeEdges of G,E; :: thesis: not G2 is locally-finite
consider v1 being Vertex of G such that
A1: v1 .edgesInOut() is infinite by Def5;
reconsider v2 = v1 as Vertex of G2 by GLIB_000:53;
v2 .edgesInOut() = (v1 .edgesInOut()) \ E by GLIBPRE0:42;
hence not G2 is locally-finite by A1; :: thesis: verum