let G be _Graph; :: thesis: ( G is locally-finite iff for v being Vertex of G holds
( v .edgesIn() is finite & v .edgesOut() is finite ) )
hereby :: thesis: ( ( for v being Vertex of G holds
( v .edgesIn() is finite & v .edgesOut() is finite ) ) implies G is locally-finite )
assume A1: G is locally-finite ; :: thesis: for v being Vertex of G holds
( v .edgesIn() is finite & v .edgesOut() is finite )
let v be Vertex of G; :: thesis: ( v .edgesIn() is finite & v .edgesOut() is finite )
v .edgesInOut() is finite by A1;
hence ( v .edgesIn() is finite & v .edgesOut() is finite ) ; :: thesis: verum
end;
assume A2: for v being Vertex of G holds
( v .edgesIn() is finite & v .edgesOut() 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 .edgesIn() is finite & v .edgesOut() is finite ) by A2;
hence v .edgesInOut() is finite ; :: thesis: verum