for G1, G2 being _Graph
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 ) )