let G2 be removeDParallelEdges of G; :: thesis: ( G2 is spanning & G2 is non-Dmulti )
consider E being RepDEdgeSelection of G such that
A3: G2 is inducedSubgraph of G, the_Vertices_of G,E by Def8;
set E2 = the RepDEdgeSelection of G2;
E c= the_Edges_of G ;
then A4: 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 A3, A4, GLIB_000:def 37;
then the_Edges_of G2 = the RepDEdgeSelection of G2 by A3, Th83;
hence ( G2 is spanning & G2 is non-Dmulti ) by A3, Th77; :: thesis: verum