let G1, G2 be _Graph; :: thesis: for G3 being removeDParallelEdges of G1 st G2 == G3 holds

G2 is removeDParallelEdges of G1

let G3 be removeDParallelEdges of G1; :: thesis: ( G2 == G3 implies G2 is removeDParallelEdges of G1 )

consider E being RepDEdgeSelection of G1 such that

A1: G3 is inducedSubgraph of G1, the_Vertices_of G1,E by Def8;

assume G2 == G3 ; :: thesis: G2 is removeDParallelEdges of G1

then G2 is inducedSubgraph of G1, the_Vertices_of G1,E by A1, GLIB_006:16;

hence G2 is removeDParallelEdges of G1 by Def8; :: thesis: verum

G2 is removeDParallelEdges of G1

let G3 be removeDParallelEdges of G1; :: thesis: ( G2 == G3 implies G2 is removeDParallelEdges of G1 )

consider E being RepDEdgeSelection of G1 such that

A1: G3 is inducedSubgraph of G1, the_Vertices_of G1,E by Def8;

assume G2 == G3 ; :: thesis: G2 is removeDParallelEdges of G1

then G2 is inducedSubgraph of G1, the_Vertices_of G1,E by A1, GLIB_006:16;

hence G2 is removeDParallelEdges of G1 by Def8; :: thesis: verum