theorem Th136: :: GLIB_000:136

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