let G be _Graph; :: thesis: for v, w being Vertex of G st w is with_max_in_degree holds
v .inDegree() c= w .inDegree()
let v, w be Vertex of G; :: thesis: ( w is with_max_in_degree implies v .inDegree() c= w .inDegree() )
assume w is with_max_in_degree ; :: thesis: v .inDegree() c= w .inDegree()
then w .inDegree() = G .supInDegree() ;
then consider v0 being Vertex of G such that
A1: v0 .inDegree() = w .inDegree() and
A2: for u being Vertex of G holds u .inDegree() c= v0 .inDegree() by Th80, Lm4;
thus v .inDegree() c= w .inDegree() by A1, A2; :: thesis: verum