theorem :: GLIB_009:39

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