theorem Th18: :: GLIB_009:18

for G being _Graph holds
( G is loopless iff for v, e being object holds not e SJoins {v},{v},G )