let G2 be reverseEdgeDirections of G,E; :: thesis: G2 is locally-finite
let v2 be Vertex of G2; :: according to GLIB_013:def 5 :: thesis: v2 .edgesInOut() is finite
reconsider v1 = v2 as Vertex of G by GLIB_007:4;
v1 .edgesInOut() = v2 .edgesInOut() by GLIB_007:12;
hence v2 .edgesInOut() is finite ; :: thesis: verum