:: deftheorem Def12 defines edgeless GLIB_014:def 12 :
for S being Graph-membered set holds
( S is edgeless iff for G being _Graph st G in S holds
G is edgeless );