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

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

assume A1: G is loopfull ; :: thesis: for v being Vertex of G holds v,v are_adjacent
let v be Vertex of G; :: thesis: v,v are_adjacent
consider e being object such that
A2: e Joins v,v,G by A1;
thus v,v are_adjacent by A2, CHORD:def 3; :: thesis: verum

end;

assume A3: for v being Vertex of G holds v,v are_adjacent ; :: thesis: G is loopfull
let v be Vertex of G; :: according to GLIB_012:def 1 :: thesis: ex e being object st e Joins v,v,G
consider e being object such that
A4: e Joins v,v,G by A3, CHORD:def 3;
take e ; :: thesis: e Joins v,v,G
thus e Joins v,v,G by A4; :: thesis: verum