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

proof

let e be object ; :: thesis: ( e in G .edgesBetween (X \ {v}) iff e in (G .edgesBetween X) \ (v .edgesInOut()) )
set u = (the_Source_of G) . e;
set w = (the_Target_of G) . e;

hereby :: thesis: ( e in (G .edgesBetween X) \ (v .edgesInOut()) implies e in G .edgesBetween (X \ {v}) )

assume e in G .edgesBetween (X \ {v}) ; :: thesis: e in (G .edgesBetween X) \ (v .edgesInOut())
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 Lm5;
then A2: e in G .edgesBetween X by Lm5;
not e in v .edgesInOut()

proof

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

end;

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

end;

assume e in (G .edgesBetween X) \ (v .edgesInOut()) ; :: thesis: e in G .edgesBetween (X \ {v})
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 Lm5;
( (the_Source_of G) . e <> v & (the_Target_of G) . e <> v ) by A3, Th61;
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, Lm5; :: thesis: verum

end;

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