theorem Th3: :: GLUNIR00:3

for G being _Graph holds
( G is loopless iff VertexDomRel G is irreflexive )