let G be finite Graph; :: thesis: for v being Vertex of G
for X2, X1 being set st X2 c= X1 holds
card (Edges_In v,(X1 \ X2)) = (card (Edges_In v,X1)) - (card (Edges_In v,X2))
let v be Vertex of G; :: thesis: for X2, X1 being set st X2 c= X1 holds
card (Edges_In v,(X1 \ X2)) = (card (Edges_In v,X1)) - (card (Edges_In v,X2))
let X2, X1 be set ; :: thesis: ( X2 c= X1 implies card (Edges_In v,(X1 \ X2)) = (card (Edges_In v,X1)) - (card (Edges_In v,X2)) )
assume A1: X2 c= X1 ; :: thesis: card (Edges_In v,(X1 \ X2)) = (card (Edges_In v,X1)) - (card (Edges_In v,X2))
then A2: X1 = X2 \/ (X1 \ X2) by XBOOLE_1:45;
set E = the carrier' of G;

now

let x be set ; :: thesis: ( ( x in Edges_In v,X1 implies x in (Edges_In v,X2) \/ (Edges_In v,(X1 \ X2)) ) & ( x in (Edges_In v,X2) \/ (Edges_In v,(X1 \ X2)) implies x in Edges_In v,X1 ) )

hereby :: thesis: ( x in (Edges_In v,X2) \/ (Edges_In v,(X1 \ X2)) implies x in Edges_In v,X1 )

assume x in Edges_In v,X1 ; :: thesis: x in (Edges_In v,X2) \/ (Edges_In v,(X1 \ X2))
then A3: ( x in the carrier' of G & x in X1 & the Target of G . x = v ) by Def1;
then ( x in X2 or x in X1 \ X2 ) by A2, XBOOLE_0:def 3;
then ( x in Edges_In v,X2 or x in Edges_In v,(X1 \ X2) ) by A3, Def1;
hence x in (Edges_In v,X2) \/ (Edges_In v,(X1 \ X2)) by XBOOLE_0:def 3; :: thesis: verum

end;

assume x in (Edges_In v,X2) \/ (Edges_In v,(X1 \ X2)) ; :: thesis: x in Edges_In v,X1
then ( x in Edges_In v,X2 or x in Edges_In v,(X1 \ X2) ) by XBOOLE_0:def 3;
then ( x in the carrier' of G & the Target of G . x = v & ( x in X2 or x in X1 \ X2 ) ) by Def1;
hence x in Edges_In v,X1 by A1, Def1; :: thesis: verum

end;

then A4: Edges_In v,X1 = (Edges_In v,X2) \/ (Edges_In v,(X1 \ X2)) by TARSKI:2;
Edges_In v,X2 misses Edges_In v,(X1 \ X2)

proof

assume not Edges_In v,X2 misses Edges_In v,(X1 \ X2) ; :: thesis: contradiction
then consider x being set such that
A5: x in (Edges_In v,X2) /\ (Edges_In v,(X1 \ X2)) by XBOOLE_0:4;
( x in Edges_In v,X2 & x in Edges_In v,(X1 \ X2) ) by A5, XBOOLE_0:def 4;
then ( x in X2 & x in X1 \ X2 ) by Def1;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

then card (Edges_In v,X1) = (card (Edges_In v,X2)) + (card (Edges_In v,(X1 \ X2))) by A4, CARD_2:53;
hence card (Edges_In v,(X1 \ X2)) = (card (Edges_In v,X1)) - (card (Edges_In v,X2)) ; :: thesis: verum