theorem Th58: :: GLIBPRE0:52

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & E c= the_Edges_of G1 holds
( v2 .edgesIn() = ((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E) & v2 .edgesOut() = ((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E) )