theorem Th21: :: GLIB_009:21
for G being _Graph holds
( G is loopless iff for v being object holds G .edgesDBetween ({v},{v}) = {} )