let G1 be _Graph; :: thesis:
let V be set ; :: thesis:
let G2 be removeVertices of G1,V; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( V c< the_Vertices_of G1 & v1 = v2 ) ; :: thesis:
then A2: the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) by Th49;
the_Vertices_of G2 = (the_Vertices_of G1) \ V by A1, Th49;
then A3: not v2 in V by XBOOLE_0:def 5;

let e be object ; :: thesis:

hereby :: thesis:

assume A4: e in v2 .edgesIn() ; :: thesis:
then A5: e in v1 .edgesIn() by A1, Th78, TARSKI:def 3;
e in G1 .edgesOutOf ((the_Vertices_of G1) \ V) by A2, A4, XBOOLE_0:def 4;
then (the_Source_of G1) . e in (the_Vertices_of G1) \ V by Def27;
then not (the_Source_of G1) . e in V by XBOOLE_0:def 5;
then not e in G1 .edgesOutOf V by Def27;
hence e in (v1 .edgesIn()) \ (G1 .edgesOutOf V) by A5, XBOOLE_0:def 5; :: thesis:

end;

assume e in (v1 .edgesIn()) \ (G1 .edgesOutOf V) ; :: thesis:
then A6: ( e in v1 .edgesIn() & not e in G1 .edgesOutOf V ) by XBOOLE_0:def 5;
then A7: not (the_Source_of G1) . e in V by Def27;
e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A6;
then A8: ( (the_Source_of G1) . e in the_Vertices_of G1 & (the_Target_of G1) . e in the_Vertices_of G1 ) by FUNCT_2:5;
then (the_Source_of G1) . e in (the_Vertices_of G1) \ V by A7, XBOOLE_0:def 5;
then A9: e in G1 .edgesOutOf ((the_Vertices_of G1) \ V) by A6, Def27;
not (the_Target_of G1) . e in V by A1, A3, A6, Lm7;
then (the_Target_of G1) . e in (the_Vertices_of G1) \ V by A8, XBOOLE_0:def 5;
then e in G1 .edgesInto ((the_Vertices_of G1) \ V) by A6, Def26;
then A10: e in the_Edges_of G2 by A2, A9, XBOOLE_0:def 4;
v1 = (the_Target_of G1) . e by A6, Lm7
.= (the_Target_of G2) . e by A10, Def32 ;
hence e in v2 .edgesIn() by A1, A10, Lm7; :: thesis:

end;

hence A11: v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) by TARSKI:2; :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

assume A12: e in v2 .edgesOut() ; :: thesis:
then A13: e in v1 .edgesOut() by A1, Th78, TARSKI:def 3;
e in G1 .edgesInto ((the_Vertices_of G1) \ V) by A2, A12, XBOOLE_0:def 4;
then (the_Target_of G1) . e in (the_Vertices_of G1) \ V by Def26;
then not (the_Target_of G1) . e in V by XBOOLE_0:def 5;
then not e in G1 .edgesInto V by Def26;
hence e in (v1 .edgesOut()) \ (G1 .edgesInto V) by A13, XBOOLE_0:def 5; :: thesis:

end;

assume e in (v1 .edgesOut()) \ (G1 .edgesInto V) ; :: thesis:
then A14: ( e in v1 .edgesOut() & not e in G1 .edgesInto V ) by XBOOLE_0:def 5;
then A15: not (the_Target_of G1) . e in V by Def26;
e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A14;
then A16: ( (the_Source_of G1) . e in the_Vertices_of G1 & (the_Target_of G1) . e in the_Vertices_of G1 ) by FUNCT_2:5;
then (the_Target_of G1) . e in (the_Vertices_of G1) \ V by A15, XBOOLE_0:def 5;
then A17: e in G1 .edgesInto ((the_Vertices_of G1) \ V) by A14, Def26;
not (the_Source_of G1) . e in V by A1, A3, A14, Lm8;
then (the_Source_of G1) . e in (the_Vertices_of G1) \ V by A16, XBOOLE_0:def 5;
then e in G1 .edgesOutOf ((the_Vertices_of G1) \ V) by A14, Def27;
then A18: e in the_Edges_of G2 by A2, A17, XBOOLE_0:def 4;
v1 = (the_Source_of G1) . e by A14, Lm8
.= (the_Source_of G2) . e by A18, Def32 ;
hence e in v2 .edgesOut() by A1, A18, Lm8; :: thesis:

end;

hence A19: v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) by TARSKI:2; :: thesis:
(v1 .edgesOut()) /\ (G1 .edgesOutOf V) = {}

assume (v1 .edgesOut()) /\ (G1 .edgesOutOf V) <> {} ; :: thesis:
then consider e being object such that
A20: e in (v1 .edgesOut()) /\ (G1 .edgesOutOf V) by XBOOLE_0:def 1;
( e in v1 .edgesOut() & e in G1 .edgesOutOf V ) by A20, XBOOLE_0:def 4;
then ( (the_Source_of G1) . e = v1 & (the_Source_of G1) . e in V ) by Def27, Lm8;
hence contradiction by A1, A3; :: thesis:

end;

then v1 .edgesOut() misses G1 .edgesOutOf V by XBOOLE_0:def 7;
then A21: (v1 .edgesOut()) \ (G1 .edgesInto V) misses G1 .edgesOutOf V by XBOOLE_1:36, XBOOLE_1:63;
(v1 .edgesIn()) /\ (G1 .edgesInto V) = {}

assume (v1 .edgesIn()) /\ (G1 .edgesInto V) <> {} ; :: thesis:
then consider e being object such that
A22: e in (v1 .edgesIn()) /\ (G1 .edgesInto V) by XBOOLE_0:def 1;
( e in v1 .edgesIn() & e in G1 .edgesInto V ) by A22, XBOOLE_0:def 4;
then ( (the_Target_of G1) . e = v1 & (the_Target_of G1) . e in V ) by Def26, Lm7;
hence contradiction by A1, A3; :: thesis:

end;

then A23: v1 .edgesIn() misses G1 .edgesInto V by XBOOLE_0:def 7;
thus v2 .edgesInOut() = ((v1 .edgesIn()) \/ ((v1 .edgesOut()) \ (G1 .edgesInto V))) \ (G1 .edgesOutOf V) by A11, A19, A21, XBOOLE_1:87
.= ((v1 .edgesInOut()) \ (G1 .edgesInto V)) \ (G1 .edgesOutOf V) by A23, XBOOLE_1:87
.= (v1 .edgesInOut()) \ (G1 .edgesInOut V) by XBOOLE_1:41 ; :: thesis: