let G1 be loopless _Graph; :: thesis: for G2 being _Graph holds
( G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1 )
let G2 be _Graph; :: thesis: ( G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1 )

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

assume G2 is DSimpleGraph of G1 ; :: thesis: G2 is removeDParallelEdges of G1
then consider E being RepDEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops()) by Def10;
thus G2 is removeDParallelEdges of G1 by A1, Def8; :: thesis: verum

end;

assume G2 is removeDParallelEdges of G1 ; :: thesis: G2 is DSimpleGraph of G1
then consider E being RepDEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def8;
E = E \ (G1 .loops()) ;
hence G2 is DSimpleGraph of G1 by A2, Def10; :: thesis: verum