:: deftheorem Def1 defines Edges_In GRAPH_3:def 1 :
for G being Graph
for v being Vertex of G
for X being set
for b₄ being Subset of the carrier' of G holds
( b₄ = Edges_In (v,X) iff for e being set holds
( e in b₄ iff ( e in the carrier' of G & e in X & the Target of G . e = v ) ) );