:: deftheorem Def2 defines loopfull GLIB_012:def 2 :
for GF being Graph-yielding Function holds
( GF is loopfull iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is loopfull ) );