theorem Th8: :: GLUNIR00:8

for G being _Graph holds
( G is edgeless iff VertexDomRel G is empty )