let G be _Graph; :: thesis: ( G is loopfull iff for v being Vertex of G ex e being object st e DJoins v,v,G )

hereby :: thesis: ( ( for v being Vertex of G ex e being object st e DJoins v,v,G ) implies G is loopfull )

assume A1: G is loopfull ; :: thesis: for v being Vertex of G ex e being object st e DJoins v,v,G
let v be Vertex of G; :: thesis: ex e being object st e DJoins v,v,G
consider e being object such that
A2: e Joins v,v,G by A1;
take e = e; :: thesis: e DJoins v,v,G
thus e DJoins v,v,G by A2, GLIB_000:16; :: thesis: verum

end;

assume A3: for v being Vertex of G ex e being object st e DJoins v,v,G ; :: 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 DJoins v,v,G by A3;
take e ; :: thesis: e Joins v,v,G
thus e Joins v,v,G by A4, GLIB_000:16; :: thesis: verum