let G1, G2 be _Graph; :: thesis: 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 ) )
let F be PGraphMapping of G1,G2; :: thesis: ( F is Dcontinuous & F is isomorphism implies ( ( 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 ) ) )
assume A1: ( F is Dcontinuous & F is isomorphism ) ; :: thesis: ( ( 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 ) )
then reconsider F0 = F as one-to-one PGraphMapping of G1,G2 ;
( F0 " is Dcontinuous & F0 " is isomorphism ) by A1, GLIB_010:74, GLIB_010:75;
hence ( ( 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 ) ) by A1, GLIB_010:50; :: thesis: verum