theorem Th28: :: GRAPH_3:28
for G being finite Graph
for v being Vertex of G
for X1, X2 being set st X2 c= X1 holds
card (Edges_Out (v,(X1 \ X2))) = (card (Edges_Out (v,X1))) - (card (Edges_Out (v,X2)))