let G1 be _Graph; :: thesis: for G2 being DSimpleGraph of G1
for G3 being SimpleGraph of G2 holds G3 is SimpleGraph of G1
let G2 be DSimpleGraph of G1; :: thesis: for G3 being SimpleGraph of G2 holds G3 is SimpleGraph of G1
let G3 be SimpleGraph of G2; :: thesis: G3 is SimpleGraph of G1
set H = the removeLoops of G1;
( G2 is removeDParallelEdges of the removeLoops of G1 & G3 is removeParallelEdges of G2 ) by Th122, Th123;
then G3 is removeParallelEdges of the removeLoops of G1 by Th95;
hence G3 is SimpleGraph of G1 by Th117; :: thesis: verum