theorem Th71: :: GLIB_000:71

for G being _Graph
for x being set
for v being Vertex of G holds
( x in v .allNeighbors() iff ex e being object st e Joins v,x,G )