let G be _Graph; :: thesis: ( G is c -Dregular implies G is c -regular )
assume A1: G is c -Dregular ; :: thesis: G is c -regular

now :: thesis: for v being Vertex of G holds v .degree() = c

let v be Vertex of G; :: thesis: v .degree() = c
thus v .degree() = (v .inDegree()) +` c by A1
.= c +` c by A1
.= c by CARD_2:75 ; :: thesis: verum

end;

hence G is c -regular ; :: thesis: verum