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

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