let G2 be removeParallelEdges of G; :: thesis: ( G2 is spanning & G2 is non-multi )
consider E being RepEdgeSelection of G such that
A1: G2 is inducedSubgraph of G, the_Vertices_of G,E by Def7;
set E2 = the RepEdgeSelection of G2;
E c= the_Edges_of G ;
then A2: 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 A1, A2, GLIB_000:def 37;
then the_Edges_of G2 = the RepEdgeSelection of G2 by A1, Th82;
hence ( G2 is spanning & G2 is non-multi ) by A1, Th75; :: thesis: verum