let c be Cardinal; :: thesis: for G being c -Dregular _Graph holds
( G .minInDegree() = c & G .minOutDegree() = c & G .maxInDegree() = c & G .maxOutDegree() = c )
let G be c -Dregular _Graph; :: thesis: ( G .minInDegree() = c & G .minOutDegree() = c & G .maxInDegree() = c & G .maxOutDegree() = c )

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

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

end;

hence G .minInDegree() = c by GLIB_013:37; :: thesis: ( G .minOutDegree() = c & G .maxInDegree() = c & G .maxOutDegree() = c )

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

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

end;

hence G .minOutDegree() = c by GLIB_013:38; :: thesis: ( G .maxInDegree() = c & G .maxOutDegree() = c )

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

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

end;

hence G .maxInDegree() = c by GLIB_013:49; :: thesis: G .maxOutDegree() = c

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

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

end;

hence G .maxOutDegree() = c by GLIB_013:50; :: thesis: verum