let G be finite Graph; :: thesis: for v being Vertex of G
for X1, X2 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 X1, X2 being set st X2 c= X1 holds
Degree (v,(X1 \ X2)) = (Degree (v,X1)) - (Degree (v,X2))
let X1, X2 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 Th27, Th28;
hence Degree (v,(X1 \ X2)) = (Degree (v,X1)) - (Degree (v,X2)) ; :: thesis: verum