theorem Th25: :: GLIB_013:25

for G being _Graph holds
( G is locally-finite iff for v being Vertex of G holds
( v .edgesIn() is finite & v .edgesOut() is finite ) )