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