theorem Th6: :: GLIB_008:6

for G being _Graph holds
( G is loopless iff for v being Vertex of G holds not v in v .allNeighbors() )