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 A1: x in Edges_In v,X ; :: thesis: x in Edges_In v,(X /\ the carrier' of G)
then x in X by Def1;
then A2: x in X /\ the carrier' of G by A1, XBOOLE_0:def 4;
the Target of G . x = v by A1, Def1;
hence x in Edges_In v,(X /\ the carrier' of G) by A1, A2, Def1; :: thesis: verum

end;

assume A3: x in Edges_In v,(X /\ the carrier' of G) ; :: thesis: 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; :: 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 A5: x in Edges_Out v,X ; :: thesis: x in Edges_Out v,(X /\ the carrier' of G)
then x in X by Def2;
then A6: x in X /\ the carrier' of G by A5, XBOOLE_0:def 4;
the Source of G . x = v by A5, Def2;
hence x in Edges_Out v,(X /\ the carrier' of G) by A5, A6, Def2; :: thesis: verum

end;

assume A7: x in Edges_Out v,(X /\ the carrier' of G) ; :: thesis: 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; :: thesis: verum

end;

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