per cases ( c is finite or c is infinite ) ;

suppose c is finite ; :: thesis: not for b₁ being _Graph holds b₁ is c -Dregular

then reconsider n = c as Nat ;
take G = the n + 1 -Dregular _Graph; :: thesis: not G is c -Dregular
assume G is c -Dregular ; :: thesis: contradiction
then n = n + 1 by Th43;
hence contradiction ; :: thesis: verum

end;

suppose A1: c is infinite ; :: thesis: not for b₁ being _Graph holds b₁ is c -Dregular

take G = the 0 -Dregular _Graph; :: thesis: not G is c -Dregular
assume G is c -Dregular ; :: thesis: contradiction
hence contradiction by A1, Th43; :: thesis: verum

end;

end;