:: deftheorem Def2 defines .loops() GLIB_009:def 2 :
for G being _Graph
for b₂ being Subset of (the_Edges_of G) holds
( b₂ = G .loops() iff for e being object holds
( e in b₂ iff ex v being object st e Joins v,v,G ) );