let G be with_max_degree _Graph; :: thesis: ( G is with_max_in_degree or G is with_max_out_degree )
consider v being Vertex of G such that
A1: v .degree() = G .supDegree() and
for w being Vertex of G holds w .degree() c= v .degree() by Th79;
set a = v .inDegree() ;
set b = v .outDegree() ;

per cases ( ( v .inDegree() c= v .outDegree() & v .outDegree() is infinite ) or ( v .outDegree() c= v .inDegree() & v .inDegree() is infinite ) or ( v .inDegree() is finite & v .outDegree() is finite ) ) ;

suppose ( v .inDegree() c= v .outDegree() & v .outDegree() is infinite ) ; :: thesis: ( G is with_max_in_degree or G is with_max_out_degree )

then v .degree() = v .outDegree() by CARD_2:76;
then A2: G .supOutDegree() c= v .outDegree() by A1, Th40;
v .outDegree() c= G .supOutDegree() by Th35;
hence ( G is with_max_in_degree or G is with_max_out_degree ) by A2, Lm5, XBOOLE_0:def 10; :: thesis: verum

end;

suppose ( v .outDegree() c= v .inDegree() & v .inDegree() is infinite ) ; :: thesis: ( G is with_max_in_degree or G is with_max_out_degree )

then v .degree() = v .inDegree() by CARD_2:76;
then A3: G .supInDegree() c= v .inDegree() by A1, Th39;
v .inDegree() c= G .supInDegree() by Th35;
hence ( G is with_max_in_degree or G is with_max_out_degree ) by A3, Lm4, XBOOLE_0:def 10; :: thesis: verum

end;

suppose ( v .inDegree() is finite & v .outDegree() is finite ) ; :: thesis: ( G is with_max_in_degree or G is with_max_out_degree )

then reconsider a = v .inDegree() , b = v .outDegree() as Nat ;

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

defpred S₁[ Nat] means ex u being Vertex of G st u .inDegree() = $1;
A4: for k being Nat st S₁[k] holds
k <= a + b

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= a + b )
given u being Vertex of G such that A5: u .inDegree() = k ; :: thesis: k <= a + b
A6: u .inDegree() c= G .supInDegree() by Th35;
G .supInDegree() c= G .supDegree() by Th39;
then Segm (u .inDegree()) c= Segm (a +` b) by A1, A6, XBOOLE_1:1;
hence k <= a + b by A5, NAT_1:39; :: thesis: verum

end;

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

proof

take a ; :: thesis: S₁[a]
take v ; :: thesis: v .inDegree() = a
thus v .inDegree() = a ; :: thesis: verum

end;

consider k being Nat such that
A8: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A4, A7);
consider u being Vertex of G such that
A9: u .inDegree() = k by A8;
take u = u; :: thesis: for w being Vertex of G holds w .inDegree() c= u .inDegree()
let w be Vertex of G; :: thesis: w .inDegree() c= u .inDegree()
A10: w .inDegree() c= G .supInDegree() by Th35;
G .supInDegree() c= G .supDegree() by Th39;
then w .inDegree() c= a +` b by A1, A10, XBOOLE_1:1;
then reconsider d = w .inDegree() as Nat ;
Segm d c= Segm k by A8, NAT_1:39;
hence w .inDegree() c= u .inDegree() by A9; :: thesis: verum

end;

hence ( G is with_max_in_degree or G is with_max_out_degree ) ; :: thesis: verum

end;

end;