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, Th74, Th75;

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, Th50; :: thesis: verum

( ( 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, Th74, Th75;

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, Th50; :: thesis: verum