let G be _Graph; :: thesis: ( G is with_max_in_degree & G is with_max_out_degree implies G is with_max_degree )
assume G is with_max_in_degree ; :: thesis: ( not G is with_max_out_degree or G is with_max_degree )
then consider v being Vertex of G such that
A1: v .inDegree() = G .supInDegree() and
A2: for u being Vertex of G holds u .inDegree() c= v .inDegree() by Th80;
assume G is with_max_out_degree ; :: thesis: G is with_max_degree
then consider w being Vertex of G such that
A3: w .outDegree() = G .supOutDegree() and
A4: for u being Vertex of G holds u .outDegree() c= w .outDegree() by Th81;
set c = G .supInDegree() ;
set d = G .supOutDegree() ;

per cases ( ( G .supOutDegree() is infinite & G .supInDegree() c= G .supOutDegree() ) or ( G .supInDegree() is infinite & G .supOutDegree() c= G .supInDegree() ) or ( G .supInDegree() is finite & G .supOutDegree() is finite ) ) ;

suppose A5: ( G .supOutDegree() is infinite & G .supInDegree() c= G .supOutDegree() ) ; :: thesis: G is with_max_degree

w .inDegree() c= G .supInDegree() by A1, A2;
then (w .inDegree()) +` (w .outDegree()) c= (G .supInDegree()) +` (w .outDegree()) by CARD_2:83;
then A6: w .degree() c= G .supOutDegree() by A3, A5, CARD_2:76;
G .supOutDegree() c= w .degree() by A3, CARD_2:94;
then A7: w .degree() = G .supOutDegree() by A6, XBOOLE_0:def 10;

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

let u be Vertex of G; :: thesis: u .degree() c= w .degree()
u .inDegree() c= v .inDegree() by A2;
then A8: u .inDegree() c= G .supOutDegree() by A1, A5, XBOOLE_1:1;
u .outDegree() c= G .supOutDegree() by A3, A4;
then u .degree() c= (G .supOutDegree()) +` (G .supOutDegree()) by A8, CARD_2:83;
hence u .degree() c= w .degree() by A5, A7, CARD_2:75; :: thesis: verum

end;

hence G is with_max_degree ; :: thesis: verum

end;

suppose A9: ( G .supInDegree() is infinite & G .supOutDegree() c= G .supInDegree() ) ; :: thesis: G is with_max_degree

v .outDegree() c= G .supOutDegree() by A3, A4;
then (v .inDegree()) +` (v .outDegree()) c= (G .supOutDegree()) +` (v .inDegree()) by CARD_2:83;
then A10: v .degree() c= G .supInDegree() by A1, A9, CARD_2:76;
G .supInDegree() c= v .degree() by A1, CARD_2:94;
then A11: v .degree() = G .supInDegree() by A10, XBOOLE_0:def 10;

now :: thesis: for u being Vertex of G holds u .degree() c= v .degree()

let u be Vertex of G; :: thesis: u .degree() c= v .degree()
A12: u .inDegree() c= v .inDegree() by A2;
u .outDegree() c= G .supOutDegree() by A3, A4;
then u .outDegree() c= G .supInDegree() by A9, XBOOLE_1:1;
then u .degree() c= (G .supInDegree()) +` (G .supInDegree()) by A1, A12, CARD_2:83;
hence u .degree() c= v .degree() by A9, A11, CARD_2:75; :: thesis: verum

end;

hence G is with_max_degree ; :: thesis: verum

end;

suppose ( G .supInDegree() is finite & G .supOutDegree() is finite ) ; :: thesis: G is with_max_degree

then reconsider c = G .supInDegree() , d = G .supOutDegree() as Nat ;
defpred S₁[ Nat] means ex u being Vertex of G st u .degree() = c₁;
A13: for k being Nat st S₁[k] holds
k <= c + d

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= c + d )
given u being Vertex of G such that A14: u .degree() = k ; :: thesis: k <= c + d
( u .inDegree() c= c & u .outDegree() c= d ) by A1, A2, A3, A4;
then u .degree() c= c +` d by CARD_2:83;
then Segm (u .degree()) c= Segm (c + d) ;
hence k <= c + d by A14, NAT_1:39; :: thesis: verum

end;

A15: ex k being Nat st S₁[k]

proof

w .inDegree() c= c by A1, A2;
then reconsider e = w .inDegree() as Nat ;
take e + d ; :: thesis: S₁[e + d]
take w ; :: thesis: w .degree() = e + d
thus w .degree() = e +` d by A3
.= e + d ; :: thesis: verum

end;

consider k being Nat such that
A16: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A13, A15);
consider u being Vertex of G such that
A17: u .degree() = k by A16;

now :: thesis: for u9 being Vertex of G holds u9 .degree() c= u .degree()

let u9 be Vertex of G; :: thesis: u9 .degree() c= u .degree()
( u9 .inDegree() c= c & u9 .outDegree() c= d ) by A1, A2, A3, A4;
then reconsider n = u9 .degree() as Nat ;
Segm n c= Segm k by A16, NAT_1:39;
hence u9 .degree() c= u .degree() by A17; :: thesis: verum

end;

hence G is with_max_degree ; :: thesis: verum

end;

end;