let G1 be _Graph; for G2 being G1 -isomorphic _Graph
for G3 being b1 -isomorphic _Graph
for F being Isomorphism of G1,G2 st G1 == G3 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 G1 == G3 holds
F " is Isomorphism of G2,G3
let G3 be G2 -isomorphic _Graph; for F being Isomorphism of G1,G2 st G1 == G3 holds
F " is Isomorphism of G2,G3
let F be Isomorphism of G1,G2; ( G1 == G3 implies F " is Isomorphism of G2,G3 )
assume A1:
G1 == G3
; F " is Isomorphism of G2,G3
G1 is reverseEdgeDirections of G1, {}
by GLIB_009:43;
then
G3 is reverseEdgeDirections of G1, {}
by A1, GLIB_007:2;
hence
F " is Isomorphism of G2,G3
by Th97; verum