let G be _Graph; :: thesis: ( G is with_max_degree implies ex v being Vertex of G st
( v .degree() = G .supDegree() & ( for w being Vertex of G holds w .degree() c= v .degree() ) ) )
assume G is with_max_degree ; :: thesis: ex v being Vertex of G st
( v .degree() = G .supDegree() & ( for w being Vertex of G holds w .degree() c= v .degree() ) )
then consider v being Vertex of G such that
A1: for w being Vertex of G holds w .degree() c= v .degree() ;
take v ; :: thesis: ( v .degree() = G .supDegree() & ( for w being Vertex of G holds w .degree() c= v .degree() ) )
set D = { (w .degree()) where w is Vertex of G : verum } ;
now :: thesis: for X being set st X in { (w .degree()) where w is Vertex of G : verum } holds
X c= v .degree()
let X be set ; :: thesis: ( X in { (w .degree()) where w is Vertex of G : verum } implies X c= v .degree() )
assume X in { (w .degree()) where w is Vertex of G : verum } ; :: thesis: X c= v .degree()
then consider w being Vertex of G such that
A2: X = w .degree() ;
thus X c= v .degree() by A1, A2; :: thesis: verum
end;
then A3: union { (w .degree()) where w is Vertex of G : verum } c= v .degree() by ZFMISC_1:76;
v .degree() c= G .supDegree() by Th35;
hence ( v .degree() = G .supDegree() & ( for w being Vertex of G holds w .degree() c= v .degree() ) ) by A1, A3, XBOOLE_0:def 10; :: thesis: verum