theorem Th65: :: GLIBPRE0:61

for G being _Graph holds
( G is edgeless iff for v, w being Vertex of G holds not v,w are_adjacent )