theorem Th35: :: GLIB_007:35

for G being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )