let G be finite Graph; :: thesis: 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)))
let v be Vertex of G; :: thesis: 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)))
let X1, X2 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;

now :: thesis: for x being object holds
( ( 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) ) )

let x be object ; :: 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 A3: x in Edges_In (v,X1) ; :: thesis: x in (Edges_In (v,X2)) \/ (Edges_In (v,(X1 \ X2)))
then x in X1 by Def1;
then A4: ( x in X2 or x in X1 \ X2 ) by A2, XBOOLE_0:def 3;
the Target of G . x = v by A3, Def1;
then ( x in Edges_In (v,X2) or x in Edges_In (v,(X1 \ X2)) ) by A3, A4, Def1;
hence x in (Edges_In (v,X2)) \/ (Edges_In (v,(X1 \ X2))) by XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

then A8: 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 object such that
A9: x in (Edges_In (v,X2)) /\ (Edges_In (v,(X1 \ X2))) by XBOOLE_0:4;
x in Edges_In (v,(X1 \ X2)) by A9, XBOOLE_0:def 4;
then A10: x in X1 \ X2 by Def1;
x in Edges_In (v,X2) by A9, XBOOLE_0:def 4;
then x in X2 by Def1;
hence contradiction by A10, 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 A8, CARD_2:40;
hence card (Edges_In (v,(X1 \ X2))) = (card (Edges_In (v,X1))) - (card (Edges_In (v,X2))) ; :: thesis: verum