theorem Th21: :: GRAPH_3:21

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