let X be set ; for G being finite Graph
for v being Vertex of G holds
( Edges_In (v,X) = Edges_In (v,(X /\ the carrier' of G)) & Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G)) )
let G be finite Graph; for v being Vertex of G holds
( Edges_In (v,X) = Edges_In (v,(X /\ the carrier' of G)) & Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G)) )
let v be Vertex of G; ( Edges_In (v,X) = Edges_In (v,(X /\ the carrier' of G)) & Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G)) )
set E = the carrier' of G;
now for x being object holds
( ( x in Edges_In (v,X) implies x in Edges_In (v,(X /\ the carrier' of G)) ) & ( x in Edges_In (v,(X /\ the carrier' of G)) implies x in Edges_In (v,X) ) )let x be
object ;
( ( x in Edges_In (v,X) implies x in Edges_In (v,(X /\ the carrier' of G)) ) & ( x in Edges_In (v,(X /\ the carrier' of G)) implies x in Edges_In (v,X) ) )assume A3:
x in Edges_In (
v,
(X /\ the carrier' of G))
;
x in Edges_In (v,X)then
x in X /\ the
carrier' of
G
by Def1;
then A4:
x in X
by XBOOLE_0:def 4;
the
Target of
G . x = v
by A3, Def1;
hence
x in Edges_In (
v,
X)
by A3, A4, Def1;
verum end;
hence
Edges_In (v,X) = Edges_In (v,(X /\ the carrier' of G))
by TARSKI:2; Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G))
now for x being object holds
( ( x in Edges_Out (v,X) implies x in Edges_Out (v,(X /\ the carrier' of G)) ) & ( x in Edges_Out (v,(X /\ the carrier' of G)) implies x in Edges_Out (v,X) ) )let x be
object ;
( ( x in Edges_Out (v,X) implies x in Edges_Out (v,(X /\ the carrier' of G)) ) & ( x in Edges_Out (v,(X /\ the carrier' of G)) implies x in Edges_Out (v,X) ) )assume A7:
x in Edges_Out (
v,
(X /\ the carrier' of G))
;
x in Edges_Out (v,X)then
x in X /\ the
carrier' of
G
by Def2;
then A8:
x in X
by XBOOLE_0:def 4;
the
Source of
G . x = v
by A7, Def2;
hence
x in Edges_Out (
v,
X)
by A7, A8, Def2;
verum end;
hence
Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G))
by TARSKI:2; verum