:: deftheorem defines EdgesIn GRAPH_1:def 21 :
for G being finite Graph
for x being Vertex of G
for b₃ being Element of NAT holds
( b₃ = EdgesIn x iff ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b₃ = card X ) );