let H be addVertices of G,V; :: thesis: H is with_max_degree
consider v0 being Vertex of G such that
A1: for w0 being Vertex of G holds w0 .degree() c= v0 .degree() by Def12;
the_Vertices_of G c= the_Vertices_of H by GLIB_006:def 9;
then reconsider v = v0 as Vertex of H by TARSKI:def 3;

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

let w be Vertex of H; :: thesis: b₁ .degree() c= v .degree()

per cases ( w in the_Vertices_of G or not w in the_Vertices_of G ) ;

suppose w in the_Vertices_of G ; :: thesis: b₁ .degree() c= v .degree()

then reconsider w0 = w as Vertex of G ;
( w .degree() = w0 .degree() & v .degree() = v0 .degree() ) by GLIBPRE0:45;
hence w .degree() c= v .degree() by A1; :: thesis: verum

end;

suppose A2: not w in the_Vertices_of G ; :: thesis: b₁ .degree() c= v .degree()

the_Vertices_of H = (the_Vertices_of G) \/ V by GLIB_006:def 10;
then w in V by A2, XBOOLE_0:def 3;
then w in V \ (the_Vertices_of G) by A2, XBOOLE_0:def 5;
then w .degree() = 0 by GLIB_006:88, GLIB_000:157;
hence w .degree() c= v .degree() by XBOOLE_1:2; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum