:: deftheorem Def1 defines loopfull GLIB_012:def 1 :
for G being _Graph holds
( G is loopfull iff for v being Vertex of G ex e being object st e Joins v,v,G );