let G be locally-finite with_max_in_degree _Graph; :: thesis: for n being Nat holds
( G .maxInDegree() = n iff ex v being Vertex of G st
( v .inDegree() = n & ( for w being Vertex of G holds w .inDegree() <= v .inDegree() ) ) )
let n be Nat; :: thesis: ( G .maxInDegree() = n iff ex v being Vertex of G st
( v .inDegree() = n & ( for w being Vertex of G holds w .inDegree() <= v .inDegree() ) ) )

hereby :: thesis: ( ex v being Vertex of G st
( v .inDegree() = n & ( for w being Vertex of G holds w .inDegree() <= v .inDegree() ) ) implies G .maxInDegree() = n )

assume G .maxInDegree() = n ; :: thesis: ex v being Vertex of G st
( v .inDegree() = n & ( for w being Vertex of G holds w .inDegree() <= v .inDegree() ) )
then consider v being Vertex of G such that
A1: v .inDegree() = n and
A2: for w being Vertex of G holds w .inDegree() c= v .inDegree() by Th80;
take v = v; :: thesis: ( v .inDegree() = n & ( for w being Vertex of G holds w .inDegree() <= v .inDegree() ) )
thus v .inDegree() = n by A1; :: thesis: for w being Vertex of G holds w .inDegree() <= v .inDegree()
let w be Vertex of G; :: thesis: w .inDegree() <= v .inDegree()
Segm (w .inDegree()) c= Segm (v .inDegree()) by A2;
hence w .inDegree() <= v .inDegree() by NAT_1:39; :: thesis: verum

end;

given v being Vertex of G such that A3: v .inDegree() = n and
A4: for w being Vertex of G holds w .inDegree() <= v .inDegree() ; :: thesis: G .maxInDegree() = n

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

let w be Vertex of G; :: thesis: w .inDegree() c= v .inDegree()
Segm (w .inDegree()) c= Segm (v .inDegree()) by A4, NAT_1:39;
hence w .inDegree() c= v .inDegree() ; :: thesis: verum

end;

hence G .maxInDegree() = n by A3, Th49; :: thesis: verum