theorem :: GLIB_009:17

for G being _Graph holds
( G is loopless iff for v, e being object holds not e DJoins v,v,G )