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

per cases ;

suppose A3: V c= the_Vertices_of G ; :: thesis:

consider v0 being Vertex of G such that
A4: for w0 being Vertex of G holds w0 .inDegree() c= v0 .inDegree() by Def13;
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 ;

suppose v0 in V ; :: thesis:

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

now :: thesis:

let w be Vertex of H; :: thesis:
reconsider w0 = w as Vertex of G by A5;

per cases ;

suppose w0 in V ; :: thesis:

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

end;

suppose not w0 in V ; :: thesis:

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

end;

end;

end;

hence H is with_max_in_degree ; :: thesis:

end;

suppose ( not v0 in V & ex w0 being Vertex of G st
( w0 in V & v0 .inDegree() c< (w0 .inDegree()) +` 1 ) ) ; :: thesis:

then consider w0 being Vertex of G such that
A9: ( w0 in V & v0 .inDegree() c< (w0 .inDegree()) +` 1 ) ;
reconsider w = w0 as Vertex of H by A5;
A10: w .inDegree() = (w0 .inDegree()) +` 1 by A3, A9, GLIB_012:43;
not (w0 .inDegree()) +` 1 c= v0 .inDegree() by A9, XBOOLE_0:def 8;
then A11: w0 .inDegree() = v0 .inDegree() by A4, Lm1;

now :: thesis:

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

per cases ;

suppose u0 in V ; :: thesis:

then A12: u .inDegree() = (u0 .inDegree()) +` 1 by A3, GLIB_012:43;
( u0 .inDegree() c= w0 .inDegree() & 1 c= 1 ) by A4, A11;
hence u .inDegree() c= w .inDegree() by A10, A12, CARD_2:83; :: thesis:

end;

suppose not u0 in V ; :: thesis:

then A13: u .inDegree() = u0 .inDegree() by A3, GLIB_012:44
.= (u0 .inDegree()) +` 0 by CARD_2:18 ;
( u0 .inDegree() c= w0 .inDegree() & 0 c= 1 ) by A4, A11, XBOOLE_1:2;
hence u .inDegree() c= w .inDegree() by A10, A13, CARD_2:83; :: thesis:

end;

end;

end;

hence H is with_max_in_degree ; :: thesis:

end;

suppose A14: ( not v0 in V & ( for w0 being Vertex of G holds
( not w0 in V or not v0 .inDegree() c< (w0 .inDegree()) +` 1 ) ) ) ; :: thesis:

then A15: v .inDegree() = v0 .inDegree() by A3, GLIB_012:44;

now :: thesis:

let w be Vertex of H; :: thesis:
reconsider w0 = w as Vertex of G by A5;

per cases ;

suppose A16: w0 in V ; :: thesis:

then w .inDegree() = (w0 .inDegree()) +` 1 by A3, GLIB_012:43;
hence w .inDegree() c= v .inDegree() by A14, A15, A16, XBOOLE_0:def 8; :: thesis:

end;

suppose not w0 in V ; :: thesis:

then w .inDegree() = w0 .inDegree() by A3, GLIB_012:44;
hence w .inDegree() c= v .inDegree() by A4, A15; :: thesis:

end;

end;

end;

hence H is with_max_in_degree ; :: thesis:

end;

end;

end;

suppose not V c= the_Vertices_of G ; :: thesis:

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

end;

end;