take G = canDCompleteGraph (c +` 1); :: thesis: ( G is Dsimple & G is c -Dregular )
thus ( G is Dsimple & G is c -Dregular ) ; :: thesis: verum