take G = canDCompleteGraph (n + 1); :: thesis: ( G is Dsimple & G is _finite & G is n -Dregular )
n + 1 = n +` 1 ;
hence ( G is Dsimple & G is _finite & G is n -Dregular ) ; :: thesis: verum