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 X2 c= X1 ; :: thesis: Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2)
then ( card (Edges_In v,(X1 \ X2)) = (card (Edges_In v,X1)) - (card (Edges_In v,X2)) & card (Edges_Out v,(X1 \ X2)) = (card (Edges_Out v,X1)) - (card (Edges_Out v,X2)) ) by Th32, Th33;
hence Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2) ; :: thesis: verum