theorem :: GLIBPRE1:64

for G2, G3 being _Graph
for V, E being set
for G1 being addVertices of G3,V
for G4 being reverseEdgeDirections of G3,E holds
( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )