let c1, c2 be Cardinal; :: thesis: for G being _Graph st G is c1 -Dregular & G is c2 -Dregular holds
c1 = c2
let G be _Graph; :: thesis: ( G is c1 -Dregular & G is c2 -Dregular implies c1 = c2 )
assume A1: ( G is c1 -Dregular & G is c2 -Dregular ) ; :: thesis: c1 = c2
set v = the Vertex of G;
thus c1 = the Vertex of G .inDegree() by A1
.= c2 by A1 ; :: thesis: verum