let G be _Graph; :: thesis: for e being object holds
( e in G .loops() iff ex v being object st e DJoins v,v,G )
let e be object ; :: thesis: ( e in G .loops() iff ex v being object st e DJoins v,v,G )

hereby :: thesis: ( ex v being object st e DJoins v,v,G implies e in G .loops() )

assume e in G .loops() ; :: thesis: ex v being object st e DJoins v,v,G
then consider v being object such that
A1: e Joins v,v,G by Def2;
take v = v; :: thesis: e DJoins v,v,G
thus e DJoins v,v,G by A1, GLIB_000:16; :: thesis: verum

end;

given v being object such that A2: e DJoins v,v,G ; :: thesis: e in G .loops()
e Joins v,v,G by A2, GLIB_000:16;
hence e in G .loops() by Def2; :: thesis: verum