let G be _Graph; :: thesis: ( G is loopless iff for v being Vertex of G holds not v,v are_adjacent )

hereby :: thesis: ( ( for v being Vertex of G holds not v,v are_adjacent ) implies G is loopless )

assume A2:
for v being Vertex of G holds not v,v are_adjacent
; :: thesis: G is loopless assume A1:
G is loopless
; :: thesis: for v being Vertex of G holds not v,v are_adjacent

let v be Vertex of G; :: thesis: not v,v are_adjacent

assume v,v are_adjacent ; :: thesis: contradiction

then ex e being object st e Joins v,v,G by CHORD:def 3;

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

end;let v be Vertex of G; :: thesis: not v,v are_adjacent

assume v,v are_adjacent ; :: thesis: contradiction

then ex e being object st e Joins v,v,G by CHORD:def 3;

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

now :: thesis: for v, e being object holds not e Joins v,v,G

hence
G is loopless
by GLIB_000:18; :: thesis: verumlet v be object ; :: thesis: for e being object holds not e Joins v,v,G

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

reconsider v0 = v as Vertex of G by A3, GLIB_000:13;

v0,v0 are_adjacent by A3, CHORD:def 3;

hence contradiction by A2; :: thesis: verum

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

reconsider v0 = v as Vertex of G by A3, GLIB_000:13;

v0,v0 are_adjacent by A3, CHORD:def 3;

hence contradiction by A2; :: thesis: verum