for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds
( F is isomorphism iff F " is isomorphism ) by Th71, Th72;