let H be removeDParallelEdges of G; :: thesis: not H is loopless
consider E being RepDEdgeSelection of G such that
A7: H is inducedSubgraph of G, the_Vertices_of G,E by GLIB_009:def 8;
consider v being object such that
A8: ex e being object st e DJoins v,v,G by GLIB_000:136;
consider e0 being object such that
A9: e0 DJoins v,v,G by A8;
consider e being object such that
A10: ( 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 A9, GLIB_009:def 6;
A11: the_Edges_of G = G .edgesBetween (the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G ;
then A12: e in the_Edges_of H by A7, A10, A11, GLIB_000:def 37;
( v is set & e is set ) by TARSKI:1;
then e DJoins v,v,H by A10, A12, GLIB_000:73;
hence not H is loopless by GLIB_000:136; :: thesis: verum