let G be _Graph; :: thesis: ( G is c +` 1 -vertex & G is Dsimple & G is Dcomplete implies G is c -Dregular )
assume A2: ( G is c +` 1 -vertex & G is Dsimple & G is Dcomplete ) ; :: thesis: G is c -Dregular
let v be Vertex of G; :: according to GLIB_016:def 8 :: thesis: ( v .inDegree() = c & v .outDegree() = c )
A3: (v .inDegree()) +` 1 = G .order() by A2, Th13
.= c +` 1 by A2, GLIB_013:def 3 ;
A4: (v .outDegree()) +` 1 = G .order() by A2, Th13
.= c +` 1 by A2, GLIB_013:def 3 ;

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

suppose A5: c is finite ; :: thesis: ( v .inDegree() = c & v .outDegree() = c )

then reconsider n = c as Nat ;
c +` 1 is finite by A5;
then ( v .inDegree() is finite & v .outDegree() is finite ) by A3, A4;
then reconsider d1 = v .inDegree() , d2 = v .outDegree() as Nat ;
( n +` 1 = n + 1 & d1 +` 1 = d1 + 1 & d2 +` 1 = d2 + 1 ) ;
then ( n + 1 = d1 + 1 & n + 1 = d2 + 1 ) by A3, A4;
hence ( v .inDegree() = c & v .outDegree() = c ) ; :: thesis: verum

end;

suppose A6: c is infinite ; :: thesis: ( v .inDegree() = c & v .outDegree() = c )

then 1 in c by CARD_3:86;
then c +` 1 = c by A6, CARD_2:76;
then A7: ( (v .inDegree()) +` 1 = c & (v .outDegree()) +` 1 = c ) by A3, A4;
then A8: ( v .inDegree() is infinite & v .outDegree() is infinite ) by A6;
then A9: ( 1 in v .inDegree() & 1 in v .outDegree() ) by CARD_3:86;
hence v .inDegree() = c by A7, A8, CARD_2:76; :: thesis: v .outDegree() = c
thus v .outDegree() = c by A7, A8, A9, CARD_2:76; :: thesis: verum

end;

end;