let G be _Graph; :: thesis:
let X be set ; :: thesis:
let v be Vertex of G; :: thesis:
for e being object holds
( e in G .edgesBetween (X \ {v}) iff e in (G .edgesBetween X) \ (v .edgesInOut()) )

let e be object ; :: thesis:
set u = (the_Source_of G) . e;
set w = (the_Target_of G) . e;

hereby :: thesis:

assume e in G .edgesBetween (X \ {v}) ; :: thesis:
then A1: ( e in the_Edges_of G & (the_Source_of G) . e in X \ {v} & (the_Target_of G) . e in X \ {v} ) by GLIB_000:31;
then A2: e in G .edgesBetween X by GLIB_000:31;
not e in v .edgesInOut()

assume e in v .edgesInOut() ; :: thesis:
then ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by GLIB_000:61;
hence contradiction by A1, ZFMISC_1:56; :: thesis:

end;

hence e in (G .edgesBetween X) \ (v .edgesInOut()) by A2, XBOOLE_0:def 5; :: thesis:

end;

assume e in (G .edgesBetween X) \ (v .edgesInOut()) ; :: thesis:
then A3: ( e in G .edgesBetween X & not e in v .edgesInOut() ) by XBOOLE_0:def 5;
then A4: ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) by GLIB_000:31;
( (the_Source_of G) . e <> v & (the_Target_of G) . e <> v ) by A3, GLIB_000:61;
then ( not (the_Source_of G) . e in {v} & not (the_Target_of G) . e in {v} ) by TARSKI:def 1;
then ( (the_Source_of G) . e in X \ {v} & (the_Target_of G) . e in X \ {v} ) by A4, XBOOLE_0:def 5;
hence e in G .edgesBetween (X \ {v}) by A3, GLIB_000:31; :: thesis:

end;

hence G .edgesBetween (X \ {v}) = (G .edgesBetween X) \ (v .edgesInOut()) by TARSKI:2; :: thesis: