theorem Th27: :: GRAPH_3:27

for G being finite Graph
for v being Vertex of G
for X1, X2 being set st X2 c= X1 holds
card (Edges_In (v,(X1 \ X2))) = (card (Edges_In (v,X1))) - (card (Edges_In (v,X2)))