:: deftheorem Def13 defines loopfull GLIB_014:def 13 :
for S being Graph-membered set holds
( S is loopfull iff for G being _Graph st G in S holds
G is loopfull );