let G be _Graph; :: thesis: for v, w being Vertex of G st w is with_max_degree holds
v .degree() c= w .degree()
let v, w be Vertex of G; :: thesis: ( w is with_max_degree implies v .degree() c= w .degree() )
assume w is with_max_degree ; :: thesis: v .degree() c= w .degree()
then w .degree() = G .supDegree() ;
then consider v0 being Vertex of G such that
A1: v0 .degree() = w .degree() and
A2: for u being Vertex of G holds u .degree() c= v0 .degree() by Th79, Lm3;
thus v .degree() c= w .degree() by A1, A2; :: thesis: verum