theorem Th137: :: GLIB_000:137

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