let G be _Graph; :: thesis: ( G is c -regular implies G is with_max_degree )
assume A1: G is c -regular ; :: thesis: G is with_max_degree
set v = the Vertex of G;

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

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

end;

hence G is with_max_degree by GLIB_013:def 12; :: thesis: verum