let G be _Graph; :: thesis: ( G is edge-finite implies ( G is with_max_degree & G is with_max_in_degree & G is with_max_out_degree ) )
assume A64: G is edge-finite ; :: thesis: ( G is with_max_degree & G is with_max_in_degree & G is with_max_out_degree )
then reconsider m = G .size() as Nat ;

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

defpred S₁[ Nat] means ex u being Vertex of G st u .degree() = c₁;
A65: for k being Nat st S₁[k] holds
k <= 2 * m

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= 2 * m )
given u being Vertex of G such that A66: u .degree() = k ; :: thesis: k <= 2 * m
( u .inDegree() c= G .size() & u .outDegree() c= G .size() ) by CARD_1:11;
then Segm (u .degree()) c= m +` m by CARD_2:83;
then Segm (u .degree()) c= Segm (2 * m) ;
hence k <= 2 * m by A66, NAT_1:39; :: thesis: verum

end;

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

proof

set v = the Vertex of G;
reconsider d = the Vertex of G .degree() as Nat by A64;
take d ; :: thesis: S₁[d]
take the Vertex of G ; :: thesis: the Vertex of G .degree() = d
thus the Vertex of G .degree() = d ; :: thesis: verum

end;

consider k being Nat such that
A68: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A65, A67);
consider u being Vertex of G such that
A69: u .degree() = k by A68;
take u = u; :: thesis: for w being Vertex of G holds w .degree() c= u .degree()
let w be Vertex of G; :: thesis: w .degree() c= u .degree()
reconsider d = w .degree() as Nat by A64;
Segm d c= Segm k by A68, NAT_1:39;
hence w .degree() c= u .degree() by A69; :: thesis: verum

end;

hence G is with_max_degree ; :: thesis: ( G is with_max_in_degree & G is with_max_out_degree )

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() = c₁;
A70: for k being Nat st S₁[k] holds
k <= m

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= m )
given u being Vertex of G such that A71: u .inDegree() = k ; :: thesis: k <= m
Segm (u .inDegree()) c= Segm m by CARD_1:11;
hence k <= m by A71, NAT_1:39; :: thesis: verum

end;

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

proof

set v = the Vertex of G;
reconsider d = the Vertex of G .inDegree() as Nat by A64;
take d ; :: thesis: S₁[d]
take the Vertex of G ; :: thesis: the Vertex of G .inDegree() = d
thus the Vertex of G .inDegree() = d ; :: thesis: verum

end;

consider k being Nat such that
A73: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A70, A72);
consider u being Vertex of G such that
A74: u .inDegree() = k by A73;
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()
reconsider d = w .inDegree() as Nat by A64;
Segm d c= Segm k by A73, NAT_1:39;
hence w .inDegree() c= u .inDegree() by A74; :: thesis: verum

end;

hence G is with_max_in_degree ; :: thesis: G is with_max_out_degree

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

defpred S₁[ Nat] means ex u being Vertex of G st u .outDegree() = c₁;
A75: for k being Nat st S₁[k] holds
k <= m

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= m )
given u being Vertex of G such that A76: u .outDegree() = k ; :: thesis: k <= m
Segm (u .outDegree()) c= Segm m by CARD_1:11;
hence k <= m by A76, NAT_1:39; :: thesis: verum

end;

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

proof

set v = the Vertex of G;
reconsider d = the Vertex of G .outDegree() as Nat by A64;
take d ; :: thesis: S₁[d]
take the Vertex of G ; :: thesis: the Vertex of G .outDegree() = d
thus the Vertex of G .outDegree() = d ; :: thesis: verum

end;

consider k being Nat such that
A78: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A75, A77);
consider u being Vertex of G such that
A79: u .outDegree() = k by A78;
take u = u; :: thesis: for w being Vertex of G holds w .outDegree() c= u .outDegree()
let w be Vertex of G; :: thesis: w .outDegree() c= u .outDegree()
reconsider d = w .outDegree() as Nat by A64;
Segm d c= Segm k by A78, NAT_1:39;
hence w .outDegree() c= u .outDegree() by A79; :: thesis: verum

end;

hence G is with_max_out_degree ; :: thesis: verum