let G be _Graph; :: thesis: ( G is locally-finite iff for v being Vertex of G holds v .degree() is finite )

hereby :: thesis: ( ( for v being Vertex of G holds v .degree() is finite ) implies G is locally-finite )

assume A1: G is locally-finite ; :: thesis: for v being Vertex of G holds v .degree() is finite
let v be Vertex of G; :: thesis: v .degree() is finite
v .edgesInOut() is finite by A1;
then ( v .edgesIn() is finite & v .edgesOut() is finite ) ;
hence v .degree() is finite ; :: thesis: verum

end;

assume A2: for v being Vertex of G holds v .degree() is finite ; :: thesis: G is locally-finite
let v be Vertex of G; :: according to GLIB_013:def 5 :: thesis: v .edgesInOut() is finite
v .degree() is finite by A2;
then ( v .edgesIn() is finite & v .edgesOut() is finite ) ;
hence v .edgesInOut() is finite ; :: thesis: verum