let G1 be _Graph; :: thesis: for G2 being G1 -isomorphic _Graph

for G3 being b_{1} -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

for G3 being b

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