theorem :: GLIB_000:112

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