theorem :: GLIB_007:37

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 w being object holds
( w is Vertex of G1 iff w is Vertex of G2 ) by Th32;