theorem :: GLIB_009:132

for G1, G2 being _Graph
for G3 being DSimpleGraph of G1 st G2 == G3 holds
G2 is DSimpleGraph of G1