theorem Th65: :: GLIBPRE0:59

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