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