let G2 be Subgraph of G; :: thesis: G2 is locally-finite
let v2 be Vertex of G2; :: according to GLIB_013:def 5 :: thesis: v2 .edgesInOut() is finite
the_Vertices_of G2 c= the_Vertices_of G ;
then reconsider v1 = v2 as Vertex of G by TARSKI:def 3;
A1: v2 .edgesInOut() c= v1 .edgesInOut() by GLIB_000:78;
v1 .edgesInOut() is finite by Def5;
hence v2 .edgesInOut() is finite by A1; :: thesis: verum