:: deftheorem Def18 defines loopless GLIB_000:def 18 :
for G being _Graph holds
( G is loopless iff for e being object holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) );