let G be finite Graph; :: thesis: for v being Vertex of G
for X2, X1 being set st X2 c= X1 holds
Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2)
let v be Vertex of G; :: thesis: for X2, X1 being set st X2 c= X1 holds
Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2)
let X2, X1 be set ; :: thesis: ( X2 c= X1 implies Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2) )
assume A1: X2 c= X1 ; :: thesis: Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2)
A2: card (Edges_In v,(X1 \ X2)) = (card (Edges_In v,X1)) - (card (Edges_In v,X2)) by A1, Th32;
card (Edges_Out v,(X1 \ X2)) = (card (Edges_Out v,X1)) - (card (Edges_Out v,X2)) by A1, Th33;
hence Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2) by A2; :: thesis: verum