theorem Th7: :: GLIB_008:7

for G being _Graph
for v being Vertex of G holds
( v is isolated iff v .allNeighbors() = {} )