let H be addEdge of G,v,e,w; :: thesis: H is with_max_out_degree

per cases ( ( v is Vertex of G & w is Vertex of G & not e in the_Edges_of G ) or not v is Vertex of G or not w is Vertex of G or e in the_Edges_of G ) ;

suppose A1: ( v is Vertex of G & w is Vertex of G & not e in the_Edges_of G ) ; :: thesis: H is with_max_out_degree

then reconsider v1 = v, w1 = w as Vertex of G ;
consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0 .outDegree() c= v0 .outDegree() by Def14;
A3: the_Vertices_of G = the_Vertices_of H by A1, GLIB_006:def 11;
then reconsider v9 = v0, v2 = v1, w2 = w1 as Vertex of H ;

per cases ( ( v <> w & v0 .outDegree() = v1 .outDegree() ) or ( v <> w & v0 .outDegree() <> v1 .outDegree() ) or v = w ) ;

suppose A4: ( v <> w & v0 .outDegree() = v1 .outDegree() ) ; :: thesis: H is with_max_out_degree

now :: thesis: for u being Vertex of H holds u .outDegree() c= v2 .outDegree()

let u be Vertex of H; :: thesis: b₁ .outDegree() c= v2 .outDegree()
reconsider u0 = u as Vertex of G by A3;

per cases ( u0 = v or u0 = w or ( u0 <> v & u0 <> w ) ) ;

suppose u0 = v ; :: thesis: b₁ .outDegree() c= v2 .outDegree()

hence u .outDegree() c= v2 .outDegree() ; :: thesis: verum

end;

suppose u0 = w ; :: thesis: b₁ .outDegree() c= v2 .outDegree()

then A5: u .outDegree() = w1 .outDegree() by A1, A4, GLIBPRE0:48
.= (w1 .outDegree()) +` 0 by CARD_2:18 ;
( w1 .outDegree() c= v1 .outDegree() & 0 c= 1 ) by A2, A4, XBOOLE_1:2;
then (w1 .outDegree()) +` 0 c= (v1 .outDegree()) +` 1 by CARD_2:83;
hence u .outDegree() c= v2 .outDegree() by A1, A4, A5, GLIBPRE0:47; :: thesis: verum

end;

suppose ( u0 <> v & u0 <> w ) ; :: thesis: b₁ .outDegree() c= v2 .outDegree()

then A6: u .outDegree() = u0 .outDegree() by GLIBPRE0:46;
( u0 .outDegree() c= v1 .outDegree() & 0 c= 1 ) by A2, A4, XBOOLE_1:2;
then (u0 .outDegree()) +` 0 c= (v1 .outDegree()) +` 1 by CARD_2:83;
then u .outDegree() c= (v1 .outDegree()) +` 1 by A6, CARD_2:18;
hence u .outDegree() c= v2 .outDegree() by A1, A4, GLIBPRE0:47; :: thesis: verum

end;

end;

end;

hence H is with_max_out_degree ; :: thesis: verum

end;

suppose A7: ( v <> w & v0 .outDegree() <> v1 .outDegree() ) ; :: thesis: H is with_max_out_degree

A8: v0 .outDegree() = v9 .outDegree()

proof

per cases ( v0 <> w1 or v0 = w1 ) ;

suppose v0 <> w1 ; :: thesis: v0 .outDegree() = v9 .outDegree()

hence v0 .outDegree() = v9 .outDegree() by A7, GLIBPRE0:46; :: thesis: verum

end;

suppose v0 = w1 ; :: thesis: v0 .outDegree() = v9 .outDegree()

hence v0 .outDegree() = v9 .outDegree() by A1, A7, GLIBPRE0:48; :: thesis: verum

end;

end;

end;

then A9: (v1 .outDegree()) +` 1 c= v9 .outDegree() by A2, A7, Lm1;

now :: thesis: for u being Vertex of H holds u .outDegree() c= v9 .outDegree()

let u be Vertex of H; :: thesis: b₁ .outDegree() c= v9 .outDegree()
reconsider u0 = u as Vertex of G by A3;

per cases ( u0 = w or u0 = v or ( u0 <> v & u0 <> w ) ) ;

suppose u0 = w ; :: thesis: b₁ .outDegree() c= v9 .outDegree()

then u .outDegree() = w1 .outDegree() by A1, A7, GLIBPRE0:48;
hence u .outDegree() c= v9 .outDegree() by A2, A8; :: thesis: verum

end;

suppose u0 = v ; :: thesis: b₁ .outDegree() c= v9 .outDegree()

hence u .outDegree() c= v9 .outDegree() by A1, A7, A9, GLIBPRE0:47; :: thesis: verum

end;

suppose ( u0 <> v & u0 <> w ) ; :: thesis: b₁ .outDegree() c= v9 .outDegree()

then u .outDegree() = u0 .outDegree() by GLIBPRE0:46;
hence u .outDegree() c= v9 .outDegree() by A2, A8; :: thesis: verum

end;

end;

end;

hence H is with_max_out_degree ; :: thesis: verum

end;

suppose v = w ; :: thesis: H is with_max_out_degree

then H is addLoops of G,{v1} by A1, GLIB_012:27;
hence H is with_max_out_degree ; :: thesis: verum

end;

end;

end;

suppose ( not v is Vertex of G or not w is Vertex of G or e in the_Edges_of G ) ; :: thesis: H is with_max_out_degree

then G == H by GLIB_006:def 11;
hence H is with_max_out_degree by Th85; :: thesis: verum

end;

end;