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

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

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

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

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

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let G4 be reverseEdgeDirections of G2,E2; :: thesis: for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let F0 be PGraphMapping of G1,G2; :: thesis: ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

consider F being PGraphMapping of G3,G4 such that

A1: F = F0 and

( not F0 is empty implies not F is empty ) and

A2: ( F0 is total implies F is total ) and

A3: ( F0 is onto implies F is onto ) and

A4: ( F0 is one-to-one implies F is one-to-one ) and

( F0 is semi-continuous implies F is semi-continuous ) and

A5: ( F0 is continuous implies F is continuous ) by Th141;

take F ; :: thesis: ( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus F = F0 by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2, A4; :: thesis: ( ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) by A2, A4, A5; :: thesis: ( F0 is isomorphism implies F is isomorphism )

thus ( F0 is isomorphism implies F is isomorphism ) by A2, A3, A4; :: thesis: verum

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

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

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

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

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let G4 be reverseEdgeDirections of G2,E2; :: thesis: for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let F0 be PGraphMapping of G1,G2; :: thesis: ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

consider F being PGraphMapping of G3,G4 such that

A1: F = F0 and

( not F0 is empty implies not F is empty ) and

A2: ( F0 is total implies F is total ) and

A3: ( F0 is onto implies F is onto ) and

A4: ( F0 is one-to-one implies F is one-to-one ) and

( F0 is semi-continuous implies F is semi-continuous ) and

A5: ( F0 is continuous implies F is continuous ) by Th141;

take F ; :: thesis: ( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus F = F0 by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2, A4; :: thesis: ( ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) by A2, A4, A5; :: thesis: ( F0 is isomorphism implies F is isomorphism )

thus ( F0 is isomorphism implies F is isomorphism ) by A2, A3, A4; :: thesis: verum