let G be finite Graph; 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; 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 ; ( 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
; 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 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 ;
( ( 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 ( 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)
;
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;
verum
end; assume A5:
x in (Edges_In (v,X2)) \/ (Edges_In (v,(X1 \ X2)))
;
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;
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))
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)))
; verum