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;
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;
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 S1[ Nat] means ex u being Vertex of G st u .degree() = c1;
A13: for k being Nat st S1[k] holds
k <= c + d
proof
let k be Nat; :: thesis: ( S1[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 S1[k]
proof
w .inDegree() c= c by A1, A2;
then reconsider e = w .inDegree() as Nat ;
take e + d ; :: thesis: S1[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: ( S1[k] & ( for n being Nat st S1[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;