theorem :: GLIB_007:36

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
for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )