let w be Vertex of G; :: thesis: ( w is with_max_in_degree & w is with_max_out_degree implies w is with_max_degree )
assume A5: ( w is with_max_in_degree & w is with_max_out_degree ) ; :: thesis: w is with_max_degree
now :: thesis: for v being Vertex of G holds v .degree() c= w .degree()
let v be Vertex of G; :: thesis: v .degree() c= w .degree()
( v .inDegree() c= w .inDegree() & v .outDegree() c= w .outDegree() ) by A5, Th95, Th96;
hence v .degree() c= w .degree() by CARD_2:83; :: thesis: verum
end;
hence w is with_max_degree by Th48; :: thesis: verum