:: deftheorem Def26 defines .edgesInto GLIB_000:def 26 :
for G being _Graph
for X being set
for b₃ being Subset of (the_Edges_of G) holds
( b₃ = G .edgesInto X iff for e being set holds
( e in b₃ iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) );