theorem :: GLIB_010:90

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Dcontinuous & F is isomorphism holds
( ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G1 is Dsimple implies G2 is Dsimple ) & ( G2 is Dsimple implies G1 is Dsimple ) )