for G1, G2, G3, G4 being _Graph
for F being PGraphMapping of G1,G2 st ex E1, E2 being set st
( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) holds
F is PGraphMapping of G3,G4