let H be removeDParallelEdges of G; :: thesis: not H is edgeless
consider E being RepDEdgeSelection of G such that
A5: H is inducedSubgraph of G, the_Vertices_of G,E by GLIB_009:def 8;
A8: the_Edges_of G = G .edgesBetween (the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G ;
then the_Edges_of H = E by A5, A8, GLIB_000:def 37;
hence not H is edgeless ; :: thesis: verum