let G be _Graph; :: thesis: for n being Nat st ( for v being Vertex of G holds v .degree() c= n ) holds
G is with_max_degree
let n be Nat; :: thesis: ( ( for v being Vertex of G holds v .degree() c= n ) implies G is with_max_degree )
assume A1: for v being Vertex of G holds v .degree() c= n ; :: thesis: G is with_max_degree
defpred S₁[ Nat] means ex v being Vertex of G st v .degree() = $1;
A2: for k being Nat st S₁[k] holds
k <= n

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= n )
given v being Vertex of G such that A3: v .degree() = k ; :: thesis: k <= n
Segm k c= Segm n by A1, A3;
hence k <= n by NAT_1:39; :: thesis: verum

end;

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

proof

set v = the Vertex of G;
the Vertex of G .degree() is finite by A1, FINSET_1:1;
then reconsider k = the Vertex of G .degree() as Nat ;
take k ; :: thesis: S₁[k]
take the Vertex of G ; :: thesis: the Vertex of G .degree() = k
thus the Vertex of G .degree() = k ; :: thesis: verum

end;

consider k being Nat such that
A5: ( S₁[k] & ( for i being Nat st S₁[i] holds
i <= k ) ) from NAT_1:sch 6(A2, A4);
consider v being Vertex of G such that
A6: v .degree() = k by A5;

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

let w be Vertex of G; :: thesis: w .degree() c= v .degree()
w .degree() is finite by A1, FINSET_1:1;
then reconsider i = w .degree() as Nat ;
Segm i c= Segm k by A5, NAT_1:39;
hence w .degree() c= v .degree() by A6; :: thesis: verum

end;

hence G is with_max_degree ; :: thesis: verum