for G being Graph
for v being Vertex of G
for X being set holds Edges_In (v,X) c= Edges_In v