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 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;

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

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

let 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;

hence G is loopless by GLIB_000:18; :: thesis: verum