theorem Th139: :: GLIB_000:139

for G being _Graph holds
( G is loopless iff for v being object holds G .edgesBetween ({v},{v}) = {} )