let G be _Graph; :: thesis: ( G is with_max_in_degree implies ex v being Vertex of G st
( v .inDegree() = G .supInDegree() & ( for w being Vertex of G holds w .inDegree() c= v .inDegree() ) ) )
assume G is with_max_in_degree ; :: thesis: ex v being Vertex of G st
( v .inDegree() = G .supInDegree() & ( for w being Vertex of G holds w .inDegree() c= v .inDegree() ) )
then consider v being Vertex of G such that
A1: for w being Vertex of G holds w .inDegree() c= v .inDegree() ;
take v ; :: thesis: ( v .inDegree() = G .supInDegree() & ( for w being Vertex of G holds w .inDegree() c= v .inDegree() ) )
set D = { (w .inDegree()) where w is Vertex of G : verum } ;

now :: thesis: for X being set st X in { (w .inDegree()) where w is Vertex of G : verum } holds
X c= v .inDegree()

let X be set ; :: thesis: ( X in { (w .inDegree()) where w is Vertex of G : verum } implies X c= v .inDegree() )
assume X in { (w .inDegree()) where w is Vertex of G : verum } ; :: thesis: X c= v .inDegree()
then consider w being Vertex of G such that
A2: X = w .inDegree() ;
thus X c= v .inDegree() by A1, A2; :: thesis: verum

end;

then A3: union { (w .inDegree()) where w is Vertex of G : verum } c= v .inDegree() by ZFMISC_1:76;
v .inDegree() c= G .supInDegree() by Th35;
hence ( v .inDegree() = G .supInDegree() & ( for w being Vertex of G holds w .inDegree() c= v .inDegree() ) ) by A1, A3, XBOOLE_0:def 10; :: thesis: verum