:: deftheorem Def15 defines the_Edges_of GLIB_014:def 15 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Edges_of S iff for E being object holds
( E in b₂ iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) );