let G1 be _Graph; :: thesis: for G2 being DSimpleGraph of G1 ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2
let G2 be DSimpleGraph of G1; :: thesis: ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2
set H = the removeLoops of G1;
G2 is removeDParallelEdges of the removeLoops of G1 by Th122;
then consider G3 being removeParallelEdges of the removeLoops of G1 such that
A1: G3 is removeParallelEdges of G2 by Th96;
reconsider G3 = G3 as SimpleGraph of G1 by Th117;
take G3 ; :: thesis: G3 is SimpleGraph of G2
thus G3 is SimpleGraph of G2 by A1, Th123; :: thesis: verum