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

now

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

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

assume A3: x in Edges_Out v,X1 ; :: thesis: x in (Edges_Out v,X2) \/ (Edges_Out v,(X1 \ X2))
then x in X1 by Def2;
then A4: ( x in X2 or x in X1 \ X2 ) by A2, XBOOLE_0:def 3;
the Source of G . x = v by A3, Def2;
then ( x in Edges_Out v,X2 or x in Edges_Out v,(X1 \ X2) ) by A3, A4, Def2;
hence x in (Edges_Out v,X2) \/ (Edges_Out v,(X1 \ X2)) by XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

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

proof

assume not Edges_Out v,X2 misses Edges_Out v,(X1 \ X2) ; :: thesis: contradiction
then consider x being set such that
A9: x in (Edges_Out v,X2) /\ (Edges_Out v,(X1 \ X2)) by XBOOLE_0:4;
x in Edges_Out v,(X1 \ X2) by A9, XBOOLE_0:def 4;
then A10: x in X1 \ X2 by Def2;
x in Edges_Out v,X2 by A9, XBOOLE_0:def 4;
then x in X2 by Def2;
hence contradiction by A10, XBOOLE_0:def 5; :: thesis: verum

end;

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