let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is locally-finite implies G2 is locally-finite )
assume A1: ( G1 == G2 & G1 is locally-finite ) ; :: thesis: G2 is locally-finite
let v be Vertex of G2; :: according to GLIB_013:def 5 :: thesis: v .edgesInOut() is finite
reconsider w = v as Vertex of G1 by A1, GLIB_000:def 34;
v .edgesInOut() = w .edgesInOut() by A1, GLIB_000:96;
hence v .edgesInOut() is finite by A1; :: thesis: verum