let G1 be _Graph; :: thesis:
let E be set ; :: thesis:
let G2 be removeEdges of G1,E; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: v1 = v2 ; :: thesis:
A2: the_Edges_of G2 = (the_Edges_of G1) \ E by Th53;

now :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

assume A3: e in v2 .edgesIn() ; :: thesis:
then A4: e in v1 .edgesIn() by A1, Th78, TARSKI:def 3;
not e in E by A2, A3, XBOOLE_0:def 5;
hence e in (v1 .edgesIn()) \ E by A4, XBOOLE_0:def 5; :: thesis:

end;

assume e in (v1 .edgesIn()) \ E ; :: thesis:
then A5: ( e in v1 .edgesIn() & not e in E ) by XBOOLE_0:def 5;
then A6: e in the_Edges_of G2 by A2, XBOOLE_0:def 5;
v1 = (the_Target_of G1) . e by A5, Lm7
.= (the_Target_of G2) . e by A6, Def32 ;
hence e in v2 .edgesIn() by A1, A6, Lm7; :: thesis:

end;

hence A7: v2 .edgesIn() = (v1 .edgesIn()) \ E by TARSKI:2; :: thesis:

now :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

assume A8: e in v2 .edgesOut() ; :: thesis:
then A9: e in v1 .edgesOut() by A1, Th78, TARSKI:def 3;
not e in E by A2, A8, XBOOLE_0:def 5;
hence e in (v1 .edgesOut()) \ E by A9, XBOOLE_0:def 5; :: thesis:

end;

assume e in (v1 .edgesOut()) \ E ; :: thesis:
then A10: ( e in v1 .edgesOut() & not e in E ) by XBOOLE_0:def 5;
then A11: e in the_Edges_of G2 by A2, XBOOLE_0:def 5;
v1 = (the_Source_of G1) . e by A10, Lm8
.= (the_Source_of G2) . e by A11, Def32 ;
hence e in v2 .edgesOut() by A1, A11, Lm8; :: thesis:

end;

hence A12: v2 .edgesOut() = (v1 .edgesOut()) \ E by TARSKI:2; :: thesis:
thus v2 .edgesInOut() = (v1 .edgesInOut()) \ E by A7, A12, XBOOLE_1:42; :: thesis: