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

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