let c be Cardinal; :: thesis: for G being c -regular _Graph holds
( G .minDegree() = c & G .maxDegree() = c )
let G be c -regular _Graph; :: thesis: ( G .minDegree() = c & G .maxDegree() = c )

now :: thesis: ex v being Vertex of G st
( v .degree() = c & ( for w being Vertex of G holds v .degree() c= w .degree() ) )

set v = the Vertex of G;
take v = the Vertex of G; :: thesis: ( v .degree() = c & ( for w being Vertex of G holds v .degree() c= w .degree() ) )
thus A1: v .degree() = c by Def4; :: thesis: for w being Vertex of G holds v .degree() c= w .degree()
let w be Vertex of G; :: thesis: v .degree() c= w .degree()
thus v .degree() c= w .degree() by A1, Def4; :: thesis: verum

end;

hence G .minDegree() = c by GLIB_013:36; :: thesis: G .maxDegree() = c

now :: thesis: ex v being Vertex of G st
( v .degree() = c & ( for w being Vertex of G holds w .degree() c= v .degree() ) )

set v = the Vertex of G;
take v = the Vertex of G; :: thesis: ( v .degree() = c & ( for w being Vertex of G holds w .degree() c= v .degree() ) )
thus A2: v .degree() = c by Def4; :: thesis: for w being Vertex of G holds w .degree() c= v .degree()
let w be Vertex of G; :: thesis: w .degree() c= v .degree()
thus w .degree() c= v .degree() by A2, Def4; :: thesis: verum

end;

hence G .maxDegree() = c by GLIB_013:48; :: thesis: verum