theorem Th36: :: GLUNIR00:36

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