let G1 be non-multi _Graph; :: thesis: for G2 being _Graph holds
( G1 == G2 iff G2 is removeParallelEdges of G1 )
let G2 be _Graph; :: thesis: ( G1 == G2 iff G2 is removeParallelEdges of G1 )

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

assume A1: G1 == G2 ; :: thesis: G2 is removeParallelEdges of G1
set E = the RepEdgeSelection of G1;
G1 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_000:100;
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_000:101;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, the RepEdgeSelection of G1 by Th74;
hence G2 is removeParallelEdges of G1 by Def7; :: thesis: verum

end;

assume G2 is removeParallelEdges of G1 ; :: thesis: G1 == G2
then consider E being RepEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;
G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1 by A2, Th74;
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_000:100;
hence G1 == G2 by A3, GLIB_000:93; :: thesis: verum