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

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let G2 be G1 -isomorphic _Graph; :: thesis: for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let E1, E2 be set ; :: thesis: for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let G3 be reverseEdgeDirections of G1,E1; :: thesis: for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let G4 be reverseEdgeDirections of G2,E2; :: thesis: G4 is G3 -isomorphic

consider F0 being PGraphMapping of G1,G2 such that

A1: F0 is isomorphism by Def23;

consider F being PGraphMapping of G3,G4 such that

F = F0 and

( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and

( F0 is strong_SG-embedding implies F is strong_SG-embedding ) and

A2: ( F0 is isomorphism implies F is isomorphism ) by Th142;

thus G4 is G3 -isomorphic by A1, A2; :: thesis: verum

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let G2 be G1 -isomorphic _Graph; :: thesis: for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let E1, E2 be set ; :: thesis: for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let G3 be reverseEdgeDirections of G1,E1; :: thesis: for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

let G4 be reverseEdgeDirections of G2,E2; :: thesis: G4 is G3 -isomorphic

consider F0 being PGraphMapping of G1,G2 such that

A1: F0 is isomorphism by Def23;

consider F being PGraphMapping of G3,G4 such that

F = F0 and

( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and

( F0 is strong_SG-embedding implies F is strong_SG-embedding ) and

A2: ( F0 is isomorphism implies F is isomorphism ) by Th142;

thus G4 is G3 -isomorphic by A1, A2; :: thesis: verum