let G1 be _Graph; :: thesis: for G2 being G1 -isomorphic _Graph
for G3 being b₁ -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; :: thesis: 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; :: thesis: for F being Isomorphism of G1,G2 st G1 == G3 holds
F " is Isomorphism of G2,G3
let F be Isomorphism of G1,G2; :: thesis: ( G1 == G3 implies F " is Isomorphism of G2,G3 )
assume A1: G1 == G3 ; :: thesis: 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; :: thesis: verum