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

for v, e being object holds not e Joins v,v,G

hereby :: 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 assume A1:
G is loopless
; :: thesis: for v, e being object holds not e DJoins v,v,G

let v be object ; :: thesis: for e being object holds not e DJoins v,v,G

given e being object such that A2: e DJoins v,v,G ; :: thesis: contradiction

e Joins v,v,G by A2, GLIB_000:16;

hence contradiction by A1, GLIB_000:18; :: thesis: verum

end;let v be object ; :: thesis: for e being object holds not e DJoins v,v,G

given e being object such that A2: e DJoins v,v,G ; :: thesis: contradiction

e Joins v,v,G by A2, GLIB_000:16;

hence contradiction by A1, GLIB_000:18; :: thesis: verum

for v, e being object holds not e Joins v,v,G

proof

hence
G is loopless
by GLIB_000:18; :: thesis: verum
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, GLIB_000:16;

hence contradiction by A3; :: thesis: verum

end;given e being object such that A4: e Joins v,v,G ; :: thesis: contradiction

e DJoins v,v,G by A4, GLIB_000:16;

hence contradiction by A3; :: thesis: verum