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

per cases ;

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

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 .degree() c= v0 .degree() by Def12;
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 ;

suppose A4: ( v <> w & v0 .degree() = v1 .degree() ) ; :: thesis:

now :: thesis:

let u be Vertex of H; :: thesis:
reconsider u0 = u as Vertex of G by A3;

per cases ;

suppose u0 = v ; :: thesis:

hence u .degree() c= v2 .degree() ; :: thesis:

end;

suppose u0 = w ; :: thesis:

then A5: u .degree() = (w1 .degree()) +` 1 by A1, A4, GLIBPRE0:50;
( w1 .degree() c= v1 .degree() & 1 c= 1 ) by A2, A4;
then (w1 .degree()) +` 1 c= (v1 .degree()) +` 1 by CARD_2:83;
hence u .degree() c= v2 .degree() by A1, A4, A5, GLIBPRE0:49; :: thesis:

end;

suppose ( u0 <> v & u0 <> w ) ; :: thesis:

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

end;

end;

end;

hence H is with_max_degree ; :: thesis:

end;

suppose A7: ( v <> w & v0 .degree() = w1 .degree() ) ; :: thesis:

now :: thesis:

let u be Vertex of H; :: thesis:
reconsider u0 = u as Vertex of G by A3;

per cases ;

suppose u0 = w ; :: thesis:

hence u .degree() c= w2 .degree() ; :: thesis:

end;

suppose u0 = v ; :: thesis:

then A8: u .degree() = (v1 .degree()) +` 1 by A1, A7, GLIBPRE0:49;
( v1 .degree() c= w1 .degree() & 1 c= 1 ) by A2, A7;
then (v1 .degree()) +` 1 c= (w1 .degree()) +` 1 by CARD_2:83;
hence u .degree() c= w2 .degree() by A1, A7, A8, GLIBPRE0:50; :: thesis:

end;

suppose ( u0 <> v & u0 <> w ) ; :: thesis:

then A9: u .degree() = u0 .degree() by GLIBPRE0:48;
( u0 .degree() c= w1 .degree() & 0 c= 1 ) by A2, A7, XBOOLE_1:2;
then (u0 .degree()) +` 0 c= (w1 .degree()) +` 1 by CARD_2:83;
then u .degree() c= (w1 .degree()) +` 1 by A9, CARD_2:18;
hence u .degree() c= w2 .degree() by A1, A7, GLIBPRE0:50; :: thesis:

end;

end;

end;

hence H is with_max_degree ; :: thesis:

end;

suppose A10: ( v <> w & v0 .degree() <> v1 .degree() & v0 .degree() <> w1 .degree() ) ; :: thesis:

then ( (v1 .degree()) +` 1 c= v0 .degree() & (w1 .degree()) +` 1 c= v0 .degree() ) by A2, Lm1;
then A11: ( (v1 .degree()) +` 1 c= v9 .degree() & (w1 .degree()) +` 1 c= v9 .degree() ) by A10, GLIBPRE0:48;

now :: thesis:

let u be Vertex of H; :: thesis:
reconsider u0 = u as Vertex of G by A3;

per cases ;

suppose u0 = v ; :: thesis:

hence u .degree() c= v9 .degree() by A1, A10, A11, GLIBPRE0:49; :: thesis:

end;

suppose u0 = w ; :: thesis:

hence u .degree() c= v9 .degree() by A1, A10, A11, GLIBPRE0:50; :: thesis:

end;

suppose ( u0 <> v & u0 <> w ) ; :: thesis:

then A12: u .degree() = u0 .degree() by GLIBPRE0:48;
u0 .degree() c= v0 .degree() by A2;
hence u .degree() c= v9 .degree() by A10, A12, GLIBPRE0:48; :: thesis:

end;

end;

end;

hence H is with_max_degree ; :: thesis:

end;

suppose v = w ; :: thesis:

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

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:

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

end;

end;