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

per cases ;

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

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

proof

let x be object ; :: thesis:
assume x in the_Edges_of G4 ; :: thesis:
then A6: ( x in the_Edges_of G2 & not x in v2 .edgesInOut() ) by A4, XBOOLE_0:def 5;
then A7: ( 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:

per cases ) . x = v1 or (the_Target_of G1) . x = v1 ) by GLIB_000:61;

suppose (the_Source_of G1) . x = v1 ; :: thesis:

then (the_Source_of G2) . x = v1 by A6, GLIB_000:def 32;
hence contradiction by A6, GLIB_000:61; :: thesis:

end;

suppose (the_Target_of G1) . x = v1 ; :: thesis:

then (the_Target_of G2) . x = v1 by A6, GLIB_000:def 32;
hence contradiction by A6, GLIB_000:61; :: thesis:

end;

end;

end;

then x in the_Edges_of G3 by A3, A6, XBOOLE_0:def 5;
hence x in (the_Edges_of G3) \ {e} by A7, XBOOLE_0:def 5; :: thesis:

end;

then A8: the_Edges_of G4 c= (the_Edges_of G3) \ {e} by TARSKI:def 3;
(the_Edges_of G3) \ {e} c= the_Edges_of G3 by XBOOLE_1:36;
then A9: the_Edges_of G4 c= the_Edges_of G3 by A8, XBOOLE_1:1;
G4 is Subgraph of G1 by GLIB_000:43;
then A10: G4 is Subgraph of G3 by A5, A9, GLIB_000:44;

A11: now :: thesis:

the_Vertices_of G3 c= the_Vertices_of G3 ;
hence the_Vertices_of G3 is non empty Subset of (the_Vertices_of G3) ; :: thesis:
(the_Edges_of G3) \ {e} c= the_Edges_of G3 by XBOOLE_1:36;
hence (the_Edges_of G3) \ {e} c= G3 .edgesBetween (the_Vertices_of G3) by GLIB_000:34; :: thesis:

end;

now :: thesis:

thus the_Vertices_of G4 = the_Vertices_of G3 by A5; :: thesis:
for x being object st x in (the_Edges_of G3) \ {e} holds
x in the_Edges_of G4

proof

let x be object ; :: thesis:
assume x in (the_Edges_of G3) \ {e} ; :: thesis:
then A12: ( x in the_Edges_of G3 & not x in {e} ) by XBOOLE_0:def 5;
then A13: ( x in the_Edges_of G1 & not x in v1 .edgesInOut() ) by A3, XBOOLE_0:def 5;
A14: x in the_Edges_of G2 by A1, A12, XBOOLE_0:def 5;
not x in v2 .edgesInOut() by A13, GLIB_000:78, TARSKI:def 3;
hence x in the_Edges_of G4 by A4, A14, XBOOLE_0:def 5; :: thesis:

end;

then (the_Edges_of G3) \ {e} c= the_Edges_of G4 by TARSKI:def 3;
hence the_Edges_of G4 = (the_Edges_of G3) \ {e} by A8, XBOOLE_0:def 10; :: thesis:

end;

hence G4 is removeEdge of G3,e by A10, A11, GLIB_000:def 37; :: thesis:

end;

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

then A16: G1 == G3 by Th8;
( G2 is _trivial or not v in the_Vertices_of G2 )

proof

per cases by A15;

suppose G1 is _trivial ; :: thesis:

hence ( G2 is _trivial or not v in the_Vertices_of G2 ) ; :: thesis:

end;

suppose not v in the_Vertices_of G1 ; :: thesis:

hence ( G2 is _trivial or not v in the_Vertices_of G2 ) ; :: thesis:

end;

end;

end;

then G2 == G4 by Th8;
hence G4 is removeEdge of G3,e by A16, Lm5; :: thesis:

end;

end;