theorem Th133: :: GLIB_009:133
for G1 being _Graph
for G2 being DSimpleGraph of G1
for G3 being SimpleGraph of G2 holds G3 is SimpleGraph of G1