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

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

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

end;

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

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

end;

end;