theorem Th40: :: GLUNIR00:40

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