theorem Th47: :: GLIB_009:47

for G being _Graph holds
( G is loopless iff G .loops() = {} )