let G be _Graph; :: thesis: for n being Nat st G is n -Dregular holds
G is 2 * n -regular
let n be Nat; :: thesis: ( G is n -Dregular implies G is 2 * n -regular )
assume A1: G is n -Dregular ; :: thesis: G is 2 * n -regular
let v be Vertex of G; :: according to GLIB_016:def 4 :: thesis: v .degree() = 2 * n
thus v .degree() = (v .inDegree()) +` n by A1
.= n +` n by A1
.= 2 * n ; :: thesis: verum