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 )

e Joins v,v,G by A2, GLIB_000:16;

hence e in G .loops() by Def2; :: thesis: verum

( 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() )

given v being object such that A2:
e DJoins v,v,G
; :: thesis: 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;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

e Joins v,v,G by A2, GLIB_000:16;

hence e in G .loops() by Def2; :: thesis: verum