let G be _Graph; ( G is loopless iff for v, e being object holds not e Joins v,v,G )
thus
( G is loopless implies for v, e being object holds not e Joins v,v,G )
; ( ( for v, e being object holds not e Joins v,v,G ) implies G is loopless )
assume A1:
for v, e being object holds not e Joins v,v,G
; G is loopless
hence
G is loopless
; verum