let G be _Graph; :: thesis: ( G is n -regular implies G is locally-finite )
assume G is n -regular ; :: thesis: G is locally-finite
then for v being Vertex of G holds v .degree() is finite ;
hence G is locally-finite by GLIB_013:23; :: thesis: verum