theorem :: GLIB_008:48

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