let H be reverseEdgeDirections of G; :: thesis: H is with_max_in_degree
consider v1 being Vertex of G such that
A1: for w1 being Vertex of G holds w1 .outDegree() c= v1 .outDegree() by Def14;
A2: the_Vertices_of G = the_Vertices_of H by GLIB_007:def 1;
then reconsider v2 = v1 as Vertex of H ;

now :: thesis: for w2 being Vertex of H holds w2 .inDegree() c= v2 .inDegree()

let w2 be Vertex of H; :: thesis: w2 .inDegree() c= v2 .inDegree()
reconsider w1 = w2 as Vertex of G by A2;
w1 .outDegree() c= v1 .outDegree() by A1;
then w1 .outDegree() c= v2 .inDegree() by GLIBPRE0:53;
hence w2 .inDegree() c= v2 .inDegree() by GLIBPRE0:53; :: thesis: verum

end;

hence H is with_max_in_degree ; :: thesis: verum