let G be _Graph; :: thesis: ( G is n -Dregular implies ( G is 2 * n -regular & G is locally-finite ) )
assume G is n -Dregular ; :: thesis: ( G is 2 * n -regular & G is locally-finite )
hence G is 2 * n -regular by Th46; :: thesis: G is locally-finite
hence G is locally-finite ; :: thesis: verum