let G1 be _Graph; for G2 being G1 -isomorphic _Graph
for G3 being b1 -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
let G2 be G1 -isomorphic _Graph; for G3 being G2 -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
let G3 be G2 -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
let F be Isomorphism of G1,G2; ( ex E being set st G3 is reverseEdgeDirections of G1,E implies F " is Isomorphism of G2,G3 )
given E being set such that A1:
G3 is reverseEdgeDirections of G1,E
; F " is Isomorphism of G2,G3
G2 is reverseEdgeDirections of G2, {}
by GLIB_009:43;
then reconsider F2 = F " as PGraphMapping of G2,G3 by A1, Th10;
A2:
F2 is total
A3:
F2 is onto
F2 is one-to-one
;
hence
F " is Isomorphism of G2,G3
by A2, A3; verum