let G1 be non-Dmulti _Graph; :: thesis: for G2 being _Graph holds

( G1 == G2 iff G2 is removeDParallelEdges of G1 )

let G2 be _Graph; :: thesis: ( G1 == G2 iff G2 is removeDParallelEdges of G1 )

then consider E being RepDEdgeSelection of G1 such that

A2: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def8;

G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1 by A2, Th76;

then A3: G2 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_000:34;

G1 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_006:15;

hence G1 == G2 by A3, GLIB_000:93; :: thesis: verum

( G1 == G2 iff G2 is removeDParallelEdges of G1 )

let G2 be _Graph; :: thesis: ( G1 == G2 iff G2 is removeDParallelEdges of G1 )

hereby :: thesis: ( G2 is removeDParallelEdges of G1 implies G1 == G2 )

assume
G2 is removeDParallelEdges of G1
; :: thesis: G1 == G2assume A1:
G1 == G2
; :: thesis: G2 is removeDParallelEdges of G1

set E = the RepDEdgeSelection of G1;

G1 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_006:15;

then G1 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1 by GLIB_000:34;

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

then G2 is inducedSubgraph of G1, the_Vertices_of G1, the RepDEdgeSelection of G1 by Th76;

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

end;set E = the RepDEdgeSelection of G1;

G1 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_006:15;

then G1 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1 by GLIB_000:34;

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

then G2 is inducedSubgraph of G1, the_Vertices_of G1, the RepDEdgeSelection of G1 by Th76;

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

then consider E being RepDEdgeSelection of G1 such that

A2: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def8;

G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1 by A2, Th76;

then A3: G2 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_000:34;

G1 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_006:15;

hence G1 == G2 by A3, GLIB_000:93; :: thesis: verum