for G being _Graph holds
( G is edgeless iff card (the_Edges_of G) = 0 ) ;