theorem Th9: :: GLUNIR00:9

for G being _Graph holds
( G is loopfull iff ( VertexDomRel G is total & VertexDomRel G is reflexive ) )