let G be _Graph; :: thesis: ( G is c +` 1 -vertex & G is simple & G is complete implies G is c -regular )
assume A2: ( G is c +` 1 -vertex & G is simple & G is complete ) ; :: thesis: G is c -regular
let v be Vertex of G; :: according to GLIB_016:def 4 :: thesis: v .degree() = c
A3: (v .degree()) +` 1 = G .order() by A2, GLIBPRE1:45
.= c +` 1 by A2, GLIB_013:def 3 ;

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

suppose A4: c is finite ; :: thesis: v .degree() = c

then reconsider n = c as Nat ;
c +` 1 is finite by A4;
then v .degree() is finite by A3;
then reconsider d = v .degree() as Nat ;
( n +` 1 = n + 1 & d +` 1 = d + 1 ) ;
then n + 1 = d + 1 by A3;
hence v .degree() = c ; :: thesis: verum

end;

suppose A5: c is infinite ; :: thesis: v .degree() = c

then 1 in c by CARD_3:86;
then c +` 1 = c by A5, CARD_2:76;
then A6: (v .degree()) +` 1 = c by A3;
then A7: v .degree() is infinite by A5;
then 1 in v .degree() by CARD_3:86;
hence v .degree() = c by A6, A7, CARD_2:76; :: thesis: verum

end;

end;