for G1, G2 being _Graph
for F0 being PGraphMapping of G1,G2 st F0 _E is one-to-one holds
ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )