theorem :: GLIB_009:134

for G1 being _Graph
for G2 being DSimpleGraph of G1 ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2