let H be addLoops of G,V; :: thesis: H is with_max_degree

per cases ( V c= the_Vertices_of G or not V c= the_Vertices_of G ) ;

suppose A3: V c= the_Vertices_of G ; :: thesis: H is with_max_degree

consider v0 being Vertex of G such that
A4: for w0 being Vertex of G holds w0 .degree() c= v0 .degree() by Def12;
A5: the_Vertices_of G = the_Vertices_of H by A3, GLIB_012:def 5;
then reconsider v = v0 as Vertex of H ;

per cases ( v0 in V or ( not v0 in V & ex w0 being Vertex of G st
( w0 in V & v0 .degree() c< (w0 .degree()) +` 2 ) ) or ( not v0 in V & ( for w0 being Vertex of G holds
( not w0 in V or not v0 .degree() c< (w0 .degree()) +` 2 ) ) ) ) ;

suppose v0 in V ; :: thesis: H is with_max_degree

then A6: v .degree() = (v0 .degree()) +` 2 by A3, GLIB_012:43;

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()
reconsider w0 = w as Vertex of G by A5;

per cases ( w0 in V or not w0 in V ) ;

suppose w0 in V ; :: thesis: b₁ .degree() c= v .degree()

then A7: w .degree() = (w0 .degree()) +` 2 by A3, GLIB_012:43;
( w0 .degree() c= v0 .degree() & 2 c= 2 ) by A4;
hence w .degree() c= v .degree() by A6, A7, CARD_2:83; :: thesis: verum

end;

suppose not w0 in V ; :: thesis: b₁ .degree() c= v .degree()

then A8: w .degree() = w0 .degree() by A3, GLIB_012:44
.= (w0 .degree()) +` 0 by CARD_2:18 ;
( w0 .degree() c= v0 .degree() & 0 c= 2 ) by A4, XBOOLE_1:2;
hence w .degree() c= v .degree() by A6, A8, CARD_2:83; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

suppose ( not v0 in V & ex w0 being Vertex of G st
( w0 in V & v0 .degree() c< (w0 .degree()) +` 2 ) ) ; :: thesis: H is with_max_degree

then consider w0 being Vertex of G such that
A9: ( w0 in V & v0 .degree() c< (w0 .degree()) +` 2 ) ;
reconsider w = w0 as Vertex of H by A5;
A10: w .degree() = (w0 .degree()) +` 2 by A3, A9, GLIB_012:43;

per cases ( for u0 being Vertex of G st u0 in V holds
u0 .degree() c= w0 .degree() or ex u0 being Vertex of G st
( u0 in V & not u0 .degree() c= w0 .degree() ) ) ;

suppose A11: for u0 being Vertex of G st u0 in V holds
u0 .degree() c= w0 .degree() ; :: thesis: H is with_max_degree

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

let u be Vertex of H; :: thesis: b₁ .degree() c= w .degree()
reconsider u0 = u as Vertex of G by A5;

per cases ( u0 in V or not u0 in V ) ;

suppose A12: u0 in V ; :: thesis: b₁ .degree() c= w .degree()

then A13: u .degree() = (u0 .degree()) +` 2 by A3, GLIB_012:43;
( u0 .degree() c= w0 .degree() & 2 c= 2 ) by A11, A12;
hence u .degree() c= w .degree() by A10, A13, CARD_2:83; :: thesis: verum

end;

suppose not u0 in V ; :: thesis: b₁ .degree() c= w .degree()

then u0 .degree() = u .degree() by A3, GLIB_012:44;
then u .degree() c= v0 .degree() by A4;
hence u .degree() c= w .degree() by A9, A10, XBOOLE_0:def 8, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

suppose ex u0 being Vertex of G st
( u0 in V & not u0 .degree() c= w0 .degree() ) ; :: thesis: H is with_max_degree

then consider u0 being Vertex of G such that
A14: ( u0 in V & not u0 .degree() c= w0 .degree() ) ;
reconsider u = u0 as Vertex of H by A5;
A15: u .degree() = (u0 .degree()) +` 2 by A3, A14, GLIB_012:43;
( u0 .degree() c= v0 .degree() & w0 .degree() c= v0 .degree() ) by A4;
then A16: u0 .degree() = v0 .degree() by A9, A14, Lm6;

now :: thesis: for x being Vertex of H holds x .degree() c= u .degree()

let x be Vertex of H; :: thesis: b₁ .degree() c= u .degree()
reconsider x0 = x as Vertex of G by A5;

per cases ( x0 in V or not x0 in V ) ;

suppose x0 in V ; :: thesis: b₁ .degree() c= u .degree()

then A17: x .degree() = (x0 .degree()) +` 2 by A3, GLIB_012:43;
( x0 .degree() c= u0 .degree() & 2 c= 2 ) by A4, A16;
hence x .degree() c= u .degree() by A15, A17, CARD_2:83; :: thesis: verum

end;

suppose not x0 in V ; :: thesis: b₁ .degree() c= u .degree()

then A18: x .degree() = x0 .degree() by A3, GLIB_012:44
.= (x0 .degree()) +` 0 by CARD_2:18 ;
( x0 .degree() c= u0 .degree() & 0 c= 2 ) by A4, A16, XBOOLE_1:2;
hence x .degree() c= u .degree() by A15, A18, CARD_2:83; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

end;

end;

suppose A19: ( not v0 in V & ( for w0 being Vertex of G holds
( not w0 in V or not v0 .degree() c< (w0 .degree()) +` 2 ) ) ) ; :: thesis: H is with_max_degree

then A20: v .degree() = v0 .degree() by A3, GLIB_012:44;

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()
reconsider w0 = w as Vertex of G by A5;

per cases ( w0 in V or not w0 in V ) ;

suppose A21: w0 in V ; :: thesis: b₁ .degree() c= v .degree()

then w .degree() = (w0 .degree()) +` 2 by A3, GLIB_012:43;
hence w .degree() c= v .degree() by A19, A20, A21, XBOOLE_0:def 8; :: thesis: verum

end;

suppose not w0 in V ; :: thesis: b₁ .degree() c= v .degree()

then w .degree() = w0 .degree() by A3, GLIB_012:44;
hence w .degree() c= v .degree() by A4, A20; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

end;

end;

suppose not V c= the_Vertices_of G ; :: thesis: H is with_max_degree

then G == H by GLIB_012:def 5;
hence H is with_max_degree by Th85; :: thesis: verum

end;

end;