let G be _Graph; :: thesis: ( G is c -Dregular implies ( G is with_max_in_degree & G is with_max_out_degree ) )
assume A1: G is c -Dregular ; :: thesis: ( G is with_max_in_degree & G is with_max_out_degree )
set v = the Vertex of G;

now :: thesis: for w being Vertex of G holds w .inDegree() c= the Vertex of G .inDegree()

let w be Vertex of G; :: thesis: w .inDegree() c= the Vertex of G .inDegree()
w .inDegree() = c by A1
.= the Vertex of G .inDegree() by A1 ;
hence w .inDegree() c= the Vertex of G .inDegree() ; :: thesis: verum

end;

hence G is with_max_in_degree by GLIB_013:def 13; :: thesis: G is with_max_out_degree

now :: thesis: for w being Vertex of G holds w .outDegree() c= the Vertex of G .outDegree()

let w be Vertex of G; :: thesis: w .outDegree() c= the Vertex of G .outDegree()
w .outDegree() = c by A1
.= the Vertex of G .outDegree() by A1 ;
hence w .outDegree() c= the Vertex of G .outDegree() ; :: thesis: verum

end;

hence G is with_max_out_degree by GLIB_013:def 14; :: thesis: verum