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