theorem :: GLIB_009:130

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