:: deftheorem Def1 defines edgeless GLIB_008:def 1 :
for G being _Graph holds
( G is edgeless iff the_Edges_of G = {} );