theorem :: GLUNIR00:39

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