theorem Th142: :: GLIB_010:142

for G1, G2 being _Graph
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 ) )