let X be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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

let x be set ; :: thesis: ( ( 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 ) )

hereby :: thesis: ( x in Edges_In v,(X /\ the carrier' of G) implies x in Edges_In v,X )

assume x in Edges_In v,X ; :: thesis: x in Edges_In v,(X /\ the carrier' of G)
then A1: ( x in the carrier' of G & x in X & the Target of G . x = v ) by Def1;
then x in X /\ the carrier' of G by XBOOLE_0:def 4;
hence x in Edges_In v,(X /\ the carrier' of G) by A1, Def1; :: thesis: verum

end;

assume x in Edges_In v,(X /\ the carrier' of G) ; :: thesis: x in Edges_In v,X
then A2: ( x in the carrier' of G & x in X /\ the carrier' of G & the Target of G . x = v ) by Def1;
then x in X by XBOOLE_0:def 4;
hence x in Edges_In v,X by A2, Def1; :: thesis: verum

end;

hence Edges_In v,X = Edges_In v,(X /\ the carrier' of G) by TARSKI:2; :: thesis: Edges_Out v,X = Edges_Out v,(X /\ the carrier' of G)

now

let x be set ; :: thesis: ( ( 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 ) )

hereby :: thesis: ( x in Edges_Out v,(X /\ the carrier' of G) implies x in Edges_Out v,X )

assume x in Edges_Out v,X ; :: thesis: x in Edges_Out v,(X /\ the carrier' of G)
then A3: ( x in the carrier' of G & x in X & the Source of G . x = v ) by Def2;
then x in X /\ the carrier' of G by XBOOLE_0:def 4;
hence x in Edges_Out v,(X /\ the carrier' of G) by A3, Def2; :: thesis: verum

end;

assume x in Edges_Out v,(X /\ the carrier' of G) ; :: thesis: x in Edges_Out v,X
then A4: ( x in the carrier' of G & x in X /\ the carrier' of G & the Source of G . x = v ) by Def2;
then x in X by XBOOLE_0:def 4;
hence x in Edges_Out v,X by A4, Def2; :: thesis: verum

end;

hence Edges_Out v,X = Edges_Out v,(X /\ the carrier' of G) by TARSKI:2; :: thesis: verum