let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1
for G3 being removeParallelEdges of G2 holds G3 is removeParallelEdges of G1
let G2 be removeDParallelEdges of G1; :: thesis: for G3 being removeParallelEdges of G2 holds G3 is removeParallelEdges of G1
let G3 be removeParallelEdges of G2; :: thesis: G3 is removeParallelEdges of G1
A1: G3 is Subgraph of G1 by GLIB_000:43;
consider E1 being RepDEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1,E1 by Def8;
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: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E1 ) by A2, GLIB_000:def 37;
consider E2 being RepEdgeSelection of G2 such that
A5: G3 is inducedSubgraph of G2, the_Vertices_of G2,E2 by Def7;
( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween (the_Vertices_of G2) ) by GLIB_000:34;
then A6: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 = E2 ) by A5, GLIB_000:def 37;
E2 c= the_Edges_of G1 by A1, A6, GLIB_000:def 32;
then A7: G3 is inducedSubgraph of G1, the_Vertices_of G1,E2 by A1, A3, A4, A6, GLIB_000:def 37;
E2 is RepEdgeSelection of G1 by A2, Th84;
hence G3 is removeParallelEdges of G1 by A7, Def7; :: thesis: verum