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 ( x in the_Edges_of G & not x in G .edgesInOut X ) by XBOOLE_0:def 5;
then A2: ( not (the_Source_of G) . x in X & not (the_Target_of G) . x in X ) by Th31;
( (the_Source_of G) . x in the_Vertices_of G & (the_Target_of G) . x in the_Vertices_of G ) by A1, FUNCT_2:7;
then ( (the_Source_of G) . x in (the_Vertices_of G) \ X & (the_Target_of G) . x in (the_Vertices_of G) \ X ) by A2, XBOOLE_0:def 5;
hence x in G .edgesBetween ((the_Vertices_of G) \ X) by A1, Lm6; :: thesis: verum

end;

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

end;

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