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