let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopless implies G2 is loopless ) & ( G2 is loopless implies G1 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) & ( G2 is edgeless implies G1 is edgeless ) & ( G1 is non-multi implies G2 is non-multi ) & ( G2 is non-multi implies G1 is non-multi ) & ( G1 is simple implies G2 is simple ) & ( G2 is simple implies G1 is simple ) & ( G1 is _finite implies G2 is _finite ) & ( G2 is _finite implies G1 is _finite ) & ( G1 is complete implies G2 is complete ) & ( G2 is complete implies G1 is complete ) )
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopless implies G2 is loopless ) & ( G2 is loopless implies G1 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) & ( G2 is edgeless implies G1 is edgeless ) & ( G1 is non-multi implies G2 is non-multi ) & ( G2 is non-multi implies G1 is non-multi ) & ( G1 is simple implies G2 is simple ) & ( G2 is simple implies G1 is simple ) & ( G1 is _finite implies G2 is _finite ) & ( G2 is _finite implies G1 is _finite ) & ( G1 is complete implies G2 is complete ) & ( G2 is complete implies G1 is complete ) ) )
assume A1: F is isomorphism ; :: thesis: ( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopless implies G2 is loopless ) & ( G2 is loopless implies G1 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) & ( G2 is edgeless implies G1 is edgeless ) & ( G1 is non-multi implies G2 is non-multi ) & ( G2 is non-multi implies G1 is non-multi ) & ( G1 is simple implies G2 is simple ) & ( G2 is simple implies G1 is simple ) & ( G1 is _finite implies G2 is _finite ) & ( G2 is _finite implies G1 is _finite ) & ( G1 is complete implies G2 is complete ) & ( G2 is complete implies G1 is complete ) )
then reconsider F = F as one-to-one PGraphMapping of G1,G2 ;
F " is isomorphism by A1, Th75;
hence ( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopless implies G2 is loopless ) & ( G2 is loopless implies G1 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) & ( G2 is edgeless implies G1 is edgeless ) & ( G1 is non-multi implies G2 is non-multi ) & ( G2 is non-multi implies G1 is non-multi ) & ( G1 is simple implies G2 is simple ) & ( G2 is simple implies G1 is simple ) & ( G1 is _finite implies G2 is _finite ) & ( G2 is _finite implies G1 is _finite ) & ( G1 is complete implies G2 is complete ) & ( G2 is complete implies G1 is complete ) ) by A1, Th35, Th49, Th52; :: thesis: verum