let G be _Graph; :: thesis: for X being set holds (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X)
let X be set ; :: thesis: (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X)
set EG = the_Edges_of G;
set VG = the_Vertices_of G;
set EIO = G .edgesInOut X;
set EB = G .edgesBetween ((the_Vertices_of G) \ X);

now

let x be set ; :: thesis: ( ( x in (the_Edges_of G) \ (G .edgesInOut X) implies x in G .edgesBetween ((the_Vertices_of G) \ X) ) & ( x in G .edgesBetween ((the_Vertices_of G) \ X) implies x in (the_Edges_of G) \ (G .edgesInOut X) ) )

hereby :: thesis: ( x in G .edgesBetween ((the_Vertices_of G) \ X) implies x in (the_Edges_of G) \ (G .edgesInOut X) )

assume A1: x in (the_Edges_of G) \ (G .edgesInOut X) ; :: thesis: x in G .edgesBetween ((the_Vertices_of G) \ X)
then A2: (the_Target_of G) . x in the_Vertices_of G by FUNCT_2:5;
A3: not x in G .edgesInOut X by A1, XBOOLE_0:def 5;
then not (the_Target_of G) . x in X by A1, Th31;
then A4: (the_Target_of G) . x in (the_Vertices_of G) \ X by A2, XBOOLE_0:def 5;
A5: (the_Source_of G) . x in the_Vertices_of G by A1, FUNCT_2:5;
not (the_Source_of G) . x in X by A1, A3, Th31;
then (the_Source_of G) . x in (the_Vertices_of G) \ X by A5, XBOOLE_0:def 5;
hence x in G .edgesBetween ((the_Vertices_of G) \ X) by A1, A4, Lm6; :: thesis: verum

end;

assume A6: x in G .edgesBetween ((the_Vertices_of G) \ X) ; :: thesis: x in (the_Edges_of G) \ (G .edgesInOut X)
then (the_Target_of G) . x in (the_Vertices_of G) \ X by Lm6;
then A7: not (the_Target_of G) . x in X by XBOOLE_0:def 5;
(the_Source_of G) . x in (the_Vertices_of G) \ X by A6, Lm6;
then not (the_Source_of G) . x in X by XBOOLE_0:def 5;
then not x in G .edgesInOut X by A7, Th31;
hence x in (the_Edges_of G) \ (G .edgesInOut X) by A6, XBOOLE_0:def 5; :: thesis: verum

end;

hence (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X) by TARSKI:1; :: thesis: verum