:: deftheorem Def3 defines loopless GLIB_014:def 3 :
for S being Graph-membered set holds
( S is loopless iff for G being _Graph st G in S holds
G is loopless );