for G1 being _Graph
for G2 being b₁ -isomorphic _Graph
for G3 being b₂ -isomorphic _Graph
for F being Isomorphism of G1,G2 st ex E being set st G3 is reverseEdgeDirections of G1,E holds
F " is Isomorphism of G2,G3