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 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

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

for G3 being b

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

A3:
F2 is onto
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;.= 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

proof

F2 is one-to-one
;
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;.= 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

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