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

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

assume A1: G is locally-finite ; :: thesis: for v being Vertex of G holds
( v .inDegree() is finite & v .outDegree() is finite )
let v be Vertex of G; :: thesis: ( v .inDegree() is finite & v .outDegree() is finite )
v .degree() is finite by A1, Th23;
hence ( v .inDegree() is finite & v .outDegree() is finite ) ; :: thesis: verum

end;

assume A2: for v being Vertex of G holds
( v .inDegree() is finite & v .outDegree() is finite ) ; :: thesis: G is locally-finite

now :: thesis: for v being Vertex of G holds v .degree() is finite

let v be Vertex of G; :: thesis: v .degree() is finite
( v .inDegree() is finite & v .outDegree() is finite ) by A2;
hence v .degree() is finite ; :: thesis: verum

end;

hence G is locally-finite by Th23; :: thesis: verum