let G1 be _Graph; :: thesis: for G3 being removeParallelEdges of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeParallelEdges of G2
let G3 be removeParallelEdges of G1; :: thesis: ex G2 being removeDParallelEdges of G1 st G3 is removeParallelEdges of G2
consider E2 being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1,E2 by Def7;
consider E1 being RepDEdgeSelection of G1 such that
A2: E2 c= E1 by Th73;
set G2 = the inducedSubgraph of G1, the_Vertices_of G1,E1;
reconsider G2 = the inducedSubgraph of G1, the_Vertices_of G1,E1 as removeDParallelEdges of G1 by Def8;
take G2 ; :: thesis: G3 is removeParallelEdges of G2
A3: ( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween () ) by GLIB_000:34;
then A4: G3 is Subgraph of G2 by ;
A5: ( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween () ) by GLIB_000:34;
the_Vertices_of G3 = the_Vertices_of G1 by ;
then A6: the_Vertices_of G3 = the_Vertices_of G2 by ;
A7: E2 c= the_Edges_of G2 by ;
the_Edges_of G3 = E2 by ;
then A8: G3 is inducedSubgraph of G2, the_Vertices_of G2,E2 by ;
E2 is RepEdgeSelection of G2 by ;
hence G3 is removeParallelEdges of G2 by ; :: thesis: verum