let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1 ex G3 being removeParallelEdges of G1 st G3 is removeParallelEdges of G2

let G2 be removeDParallelEdges of G1; :: thesis: ex G3 being removeParallelEdges of G1 st G3 is removeParallelEdges of G2

consider E1 being RepDEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E1 by Def8;

consider E2 being RepEdgeSelection of G1 such that

A2: E2 c= E1 by Th72;

set G3 = the inducedSubgraph of G1, the_Vertices_of G1,E2;

reconsider G3 = the inducedSubgraph of G1, the_Vertices_of G1,E2 as removeParallelEdges of G1 by Def7;

take G3 ; :: thesis: G3 is removeParallelEdges of G2

A3: ( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;

then A4: G3 is Subgraph of G2 by A1, A2, GLIB_000:46;

A5: ( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween (the_Vertices_of G2) ) by GLIB_000:34;

the_Vertices_of G2 = the_Vertices_of G1 by A1, A3, GLIB_000:def 37;

then A6: the_Vertices_of G3 = the_Vertices_of G2 by A3, GLIB_000:def 37;

A7: E2 c= the_Edges_of G2 by A1, A2, A3, GLIB_000:def 37;

the_Edges_of G3 = E2 by A3, GLIB_000:def 37;

then A8: G3 is inducedSubgraph of G2, the_Vertices_of G2,E2 by A4, A5, A6, A7, GLIB_000:def 37;

E2 is RepEdgeSelection of G2 by A7, Th78;

hence G3 is removeParallelEdges of G2 by A8, Def7; :: thesis: verum

let G2 be removeDParallelEdges of G1; :: thesis: ex G3 being removeParallelEdges of G1 st G3 is removeParallelEdges of G2

consider E1 being RepDEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E1 by Def8;

consider E2 being RepEdgeSelection of G1 such that

A2: E2 c= E1 by Th72;

set G3 = the inducedSubgraph of G1, the_Vertices_of G1,E2;

reconsider G3 = the inducedSubgraph of G1, the_Vertices_of G1,E2 as removeParallelEdges of G1 by Def7;

take G3 ; :: thesis: G3 is removeParallelEdges of G2

A3: ( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;

then A4: G3 is Subgraph of G2 by A1, A2, GLIB_000:46;

A5: ( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween (the_Vertices_of G2) ) by GLIB_000:34;

the_Vertices_of G2 = the_Vertices_of G1 by A1, A3, GLIB_000:def 37;

then A6: the_Vertices_of G3 = the_Vertices_of G2 by A3, GLIB_000:def 37;

A7: E2 c= the_Edges_of G2 by A1, A2, A3, GLIB_000:def 37;

the_Edges_of G3 = E2 by A3, GLIB_000:def 37;

then A8: G3 is inducedSubgraph of G2, the_Vertices_of G2,E2 by A4, A5, A6, A7, GLIB_000:def 37;

E2 is RepEdgeSelection of G2 by A7, Th78;

hence G3 is removeParallelEdges of G2 by A8, Def7; :: thesis: verum