let H be addVertices of G,V; :: thesis: H is with_max_out_degree
consider v0 being Vertex of G such that
A1: for w0 being Vertex of G holds w0 .outDegree() c= v0 .outDegree() by Def14;
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 .outDegree() c= v .outDegree()

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

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₁ .outDegree() c= v .outDegree()

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

end;

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

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 is isolated by GLIB_006:88;
then w .outDegree() = 0 by GLIB_000:156;
hence w .outDegree() c= v .outDegree() by XBOOLE_1:2; :: thesis: verum

end;

end;

end;

hence H is with_max_out_degree ; :: thesis: verum