theorem Th83: :: GLIBPRE0:77

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is isomorphism )