let G be _Graph; :: thesis: ( G is loopless iff for v, e being object holds not e DJoins v,v,G )
thus ( G is loopless implies for v, e being object holds not e DJoins v,v,G ) ; :: thesis: ( ( for v, e being object holds not e DJoins v,v,G ) implies G is loopless )
assume A3: for v, e being object holds not e DJoins v,v,G ; :: thesis: G is loopless
for v, e being object holds not e Joins v,v,G

proof

let v be object ; :: thesis: for e being object holds not e Joins v,v,G
given e being object such that A4: e Joins v,v,G ; :: thesis: contradiction
e DJoins v,v,G by A4;
hence contradiction by A3; :: thesis: verum

end;

hence G is loopless by Th18; :: thesis: verum