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:1; :: 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:1; :: thesis: verum