theorem :: GLIB_007:23

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) )