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 ex E being set st G3 is reverseEdgeDirections of G1,E 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 ex E being set st G3 is reverseEdgeDirections of G1,E holds
F " is Isomorphism of G2,G3
let G3 be G2 -isomorphic _Graph; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

proof

thus dom (F2 _V) = rng (F _V) by FUNCT_1:33
.= the_Vertices_of G2 by Def12 ; :: according to GLIB_010:def 11 :: thesis: dom (F2 _E) = the_Edges_of G2
thus dom (F2 _E) = rng (F _E) by FUNCT_1:33
.= the_Edges_of G2 by Def12 ; :: thesis: verum

end;

A3: F2 is onto

proof

thus rng (F2 _V) = dom (F _V) by FUNCT_1:33
.= the_Vertices_of G1 by Def11
.= the_Vertices_of G3 by A1, GLIB_007:4 ; :: according to GLIB_010:def 12 :: thesis: rng (F2 _E) = the_Edges_of G3
thus rng (F2 _E) = dom (F _E) by FUNCT_1:33
.= the_Edges_of G1 by Def11
.= the_Edges_of G3 by A1, GLIB_007:4 ; :: thesis: verum

end;

F2 is one-to-one ;
hence F " is Isomorphism of G2,G3 by A2, A3; :: thesis: verum