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

per cases ( ( not G1 is _trivial & v in the_Vertices_of G1 ) or G1 is _trivial or not v in the_Vertices_of G1 ) ;

suppose A3: ( not G1 is _trivial & v in the_Vertices_of G1 ) ; :: thesis: G4 is removeVertex of G3,v

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, Th47;
then A5: the_Edges_of G2 = (G1 .edgesBetween (the_Vertices_of G1)) \ (v1 .edgesInOut()) by Th107
.= (the_Edges_of G1) \ (v1 .edgesInOut()) by Th34 ;
A6: the_Vertices_of G4 c= the_Vertices_of G3 by A1, A2;
A7: G4 is Subgraph of G1 by Th43;
for x being object st x in the_Edges_of G4 holds
x in the_Edges_of G3

proof

let x be object ; :: thesis: ( x in the_Edges_of G4 implies x in the_Edges_of G3 )
assume x in the_Edges_of G4 ; :: thesis: x in the_Edges_of G3
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: verum

end;

then the_Edges_of G4 c= the_Edges_of G3 ;
then A8: G4 is Subgraph of G3 by A6, A7, Th44;

now :: thesis: ( the_Vertices_of G4 = (the_Vertices_of G3) \ {v} & the_Edges_of G4 = G3 .edgesBetween ((the_Vertices_of G3) \ {v}) )

thus the_Vertices_of G4 = (the_Vertices_of G3) \ {v} by A1, A2, A4; :: thesis: the_Edges_of G4 = G3 .edgesBetween ((the_Vertices_of G3) \ {v})
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: ( x in the_Edges_of G4 iff x in G3 .edgesBetween ((the_Vertices_of G3) \ {v}) )
A9: G3 .edgesBetween ((the_Vertices_of G3) \ {v}) = (G3 .edgesBetween (the_Vertices_of G3)) \ (v3 .edgesInOut()) by Th107
.= (the_Edges_of G3) \ (v3 .edgesInOut()) by Th34 ;

hereby :: thesis: ( x in G3 .edgesBetween ((the_Vertices_of G3) \ {v}) implies x in the_Edges_of G4 )

assume x in the_Edges_of G4 ; :: thesis: x in G3 .edgesBetween ((the_Vertices_of G3) \ {v})
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 Th78, 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: verum

end;

assume x in G3 .edgesBetween ((the_Vertices_of G3) \ {v}) ; :: thesis: x in the_Edges_of G4
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: contradiction
then x in (v1 .edgesInOut()) /\ (the_Edges_of G3) by A12, XBOOLE_0:def 4;
hence contradiction by A12, Th79; :: thesis: verum

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: verum

end;

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

end;

hence G4 is removeVertex of G3,v by A8, Def37; :: thesis: verum

end;

suppose A14: ( G1 is _trivial or not v in the_Vertices_of G1 ) ; :: thesis: G4 is removeVertex of G3,v

then G1 == G2 by Th114;
then A15: G3 == G4 by Lm12;
( G3 is _trivial or not v in the_Vertices_of G3 ) by A14;
hence G4 is removeVertex of G3,v by A15, Th115; :: thesis: verum

end;

end;