let G be finite Graph; :: thesis: for v being Vertex of G
for X1, X2 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 X1, X2 being set st X2 c= X1 holds
card (Edges_Out (v,(X1 \ X2))) = (card (Edges_Out (v,X1))) - (card (Edges_Out (v,X2)))
let X1, X2 be set ; :: thesis: ( X2 c= X1 implies card (Edges_Out (v,(X1 \ X2))) = (card (Edges_Out (v,X1))) - (card (Edges_Out (v,X2))) )
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 :: thesis: for x being object holds
( ( 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) ) )
let x be object ; :: 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 object 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:40;
hence card (Edges_Out (v,(X1 \ X2))) = (card (Edges_Out (v,X1))) - (card (Edges_Out (v,X2))) ; :: thesis: verum