theorem :: GLIB_012:2

for G being _Graph holds
( G is loopfull iff for v being Vertex of G holds v,v are_adjacent )