let G1 be _Graph; :: thesis:
let v, e be set ; :: thesis:
let G2 be removeVertex of G1,v; :: thesis:
let G3 be removeEdge of G1,e; :: thesis:
let G4 be removeEdge of G2,e; :: thesis:
A1: ( the_Vertices_of G3 = the_Vertices_of G1 & the_Edges_of G3 = (the_Edges_of G1) \ {e} ) by GLIB_000:51;
A2: ( the_Vertices_of G4 = the_Vertices_of G2 & the_Edges_of G4 = (the_Edges_of G2) \ {e} ) by GLIB_000:51;

per cases ;

suppose A3: ( not G1 is _trivial & v in the_Vertices_of G1 ) ; :: thesis:

then reconsider v1 = v as Vertex of G1 ;
reconsider v3 = v1 as Vertex of G3 by A1;
A4: ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) by A3, GLIB_000:47;
then A5: the_Edges_of G2 = (G1 .edgesBetween (the_Vertices_of G1)) \ (v1 .edgesInOut()) by Th1
.= (the_Edges_of G1) \ (v1 .edgesInOut()) by GLIB_000:34 ;
A6: the_Vertices_of G4 c= the_Vertices_of G3 by A1, A2;
A7: G4 is Subgraph of G1 by GLIB_000:43;
for x being object st x in the_Edges_of G4 holds
x in the_Edges_of G3

proof

let x be object ; :: thesis:
assume x in the_Edges_of G4 ; :: thesis:
then ( x in the_Edges_of G2 & not x in {e} ) by A2, XBOOLE_0:def 5;
hence x in the_Edges_of G3 by A1, XBOOLE_0:def 5; :: thesis:

end;

then the_Edges_of G4 c= the_Edges_of G3 by TARSKI:def 3;
then A8: G4 is Subgraph of G3 by A6, A7, GLIB_000:44;

now :: thesis:

thus the_Vertices_of G4 = (the_Vertices_of G3) \ {v} by A1, A2, A4; :: thesis:
for x being object holds
( x in the_Edges_of G4 iff x in G3 .edgesBetween ((the_Vertices_of G3) \ {v}) )

proof

let x be object ; :: thesis:
A9: G3 .edgesBetween ((the_Vertices_of G3) \ {v}) = (G3 .edgesBetween (the_Vertices_of G3)) \ (v3 .edgesInOut()) by Th1
.= (the_Edges_of G3) \ (v3 .edgesInOut()) by GLIB_000:34 ;

hereby :: thesis:

assume x in the_Edges_of G4 ; :: thesis:
then A10: ( x in the_Edges_of G2 & not x in {e} ) by A2, XBOOLE_0:def 5;
then ( x in the_Edges_of G1 & not x in v1 .edgesInOut() ) by A5, XBOOLE_0:def 5;
then A11: not x in v3 .edgesInOut() by GLIB_000:78, TARSKI:def 3;
x in the_Edges_of G3 by A1, A10, XBOOLE_0:def 5;
hence x in G3 .edgesBetween ((the_Vertices_of G3) \ {v}) by A9, A11, XBOOLE_0:def 5; :: thesis:

end;

assume x in G3 .edgesBetween ((the_Vertices_of G3) \ {v}) ; :: thesis:
then A12: ( x in the_Edges_of G3 & not x in v3 .edgesInOut() ) by A9, XBOOLE_0:def 5;
then A13: ( x in the_Edges_of G1 & not x in {e} ) by A1, XBOOLE_0:def 5;
not x in v1 .edgesInOut()

proof

assume x in v1 .edgesInOut() ; :: thesis:
then x in (v1 .edgesInOut()) /\ (the_Edges_of G3) by A12, XBOOLE_0:def 4;
hence contradiction by A12, GLIB_000:79; :: thesis:

end;

then x in the_Edges_of G2 by A5, A13, XBOOLE_0:def 5;
hence x in the_Edges_of G4 by A2, A13, XBOOLE_0:def 5; :: thesis:

end;

hence the_Edges_of G4 = G3 .edgesBetween ((the_Vertices_of G3) \ {v}) by TARSKI:2; :: thesis:

end;

hence G4 is removeVertex of G3,v by A8, GLIB_000:def 37; :: thesis:

end;

suppose A14: ( G1 is _trivial or not v in the_Vertices_of G1 ) ; :: thesis:

then G1 == G2 by Th8;
then A15: G3 == G4 by Lm4;
( G3 is _trivial or not v in the_Vertices_of G3 ) by A14;
hence G4 is removeVertex of G3,v by A15, Th9; :: thesis:

end;

end;