let G2 be removeDParallelEdges of G; :: thesis: G2 is loopfull
consider E being RepDEdgeSelection of G such that
A5: G2 is inducedSubgraph of G, the_Vertices_of G,E by GLIB_009:def 8;

now :: thesis: for v being Vertex of G2 ex e being object st e DJoins v,v,G2

let v be Vertex of G2; :: thesis: ex e being object st e DJoins v,v,G2
v is Vertex of G by GLIB_000:def 33;
then consider e0 being object such that
A6: e0 DJoins v,v,G by Th1;
consider e being object such that
A7: ( e DJoins v,v,G & e in E ) and
for e9 being object st e9 DJoins v,v,G & e9 in E holds
e9 = e by A6, GLIB_009:def 6;
take e = e; :: thesis: e DJoins v,v,G2
E c= the_Edges_of G ;
then A8: E c= G .edgesBetween (the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G ;
then the_Edges_of G2 = E by A5, A8, GLIB_000:def 37;
hence e DJoins v,v,G2 by A7, GLIB_000:73; :: thesis: verum

end;

hence G2 is loopfull by Th1; :: thesis: verum