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