let G be non _trivial _Graph; :: thesis:
let v1, e be object ; :: thesis:
let v2 be Vertex of G; :: thesis:
let G1 be addAdjVertex of G,v1,e,v2; :: thesis:
let G2 be removeVertex of G1,v2; :: thesis:
let G3 be removeVertex of G,v2; :: thesis:
assume A1: ( not e in the_Edges_of G & not v1 in the_Vertices_of G ) ; :: thesis:
A2: ( v2 is Vertex of G1 & v1 <> v2 ) by A1, Th72;
A3: the_Vertices_of G2 = (the_Vertices_of G1) \ {v2} by A2, GLIB_000:47
.= ((the_Vertices_of G) \/ {v1}) \ {v2} by A1, Def12
.= ((the_Vertices_of G) \ {v2}) \/ ({v1} \ {v2}) by XBOOLE_1:42
.= ((the_Vertices_of G) \ {v2}) \/ {v1} by A2, ZFMISC_1:14
.= (the_Vertices_of G3) \/ {v1} by GLIB_000:47 ;
for e1 being object holds
( e1 in G1 .edgesBetween ((the_Vertices_of G1) \ {v2}) iff e1 in G .edgesBetween ((the_Vertices_of G) \ {v2}) )

let e1 be object ; :: thesis:
set x1 = (the_Source_of G1) . e1;
set y1 = (the_Target_of G1) . e1;
set x = (the_Source_of G) . e1;
set y = (the_Target_of G) . e1;

hereby :: thesis:

assume e1 in G1 .edgesBetween ((the_Vertices_of G1) \ {v2}) ; :: thesis:
then A4: ( e1 in the_Edges_of G1 & (the_Source_of G1) . e1 in (the_Vertices_of G1) \ {v2} & (the_Target_of G1) . e1 in (the_Vertices_of G1) \ {v2} ) by GLIB_000:31;
then e1 DJoins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 by GLIB_000:def 14;

per cases by Th75;

suppose A5: e1 DJoins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G ; :: thesis:

then A6: e1 in the_Edges_of G by GLIB_000:def 14;
e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G by A5, GLIB_000:16;
then A7: ( (the_Source_of G1) . e1 in the_Vertices_of G & (the_Target_of G1) . e1 in the_Vertices_of G ) by GLIB_000:13;
( not (the_Source_of G1) . e1 in {v2} & not (the_Target_of G1) . e1 in {v2} ) by A4, XBOOLE_0:def 5;
then A8: ( (the_Source_of G1) . e1 in (the_Vertices_of G) \ {v2} & (the_Target_of G1) . e1 in (the_Vertices_of G) \ {v2} ) by A7, XBOOLE_0:def 5;
( (the_Source_of G) . e1 = (the_Source_of G1) . e1 & (the_Target_of G) . e1 = (the_Target_of G1) . e1 ) by A5, GLIB_000:def 14;
hence e1 in G .edgesBetween ((the_Vertices_of G) \ {v2}) by A6, A8, GLIB_000:31; :: thesis:

end;

suppose A9: not e1 in the_Edges_of G ; :: thesis:

the_Edges_of G1 = (the_Edges_of G) \/ {e} by A1, Def12;
then e1 in {e} by A4, A9, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A1, Th136;
then (the_Target_of G1) . e1 = v2 by GLIB_000:def 14;
then (the_Target_of G1) . e1 in {v2} by TARSKI:def 1;
hence e1 in G .edgesBetween ((the_Vertices_of G) \ {v2}) by A4, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

assume e1 in G .edgesBetween ((the_Vertices_of G) \ {v2}) ; :: thesis:
then A10: ( e1 in the_Edges_of G & (the_Source_of G) . e1 in (the_Vertices_of G) \ {v2} & (the_Target_of G) . e1 in (the_Vertices_of G) \ {v2} ) by GLIB_000:31;
the_Vertices_of G c= the_Vertices_of G1 by Def9;
then A11: ( (the_Source_of G) . e1 in (the_Vertices_of G1) \ {v2} & (the_Target_of G) . e1 in (the_Vertices_of G1) \ {v2} ) by A10, XBOOLE_1:33, TARSKI:def 3;
A12: ( (the_Source_of G) . e1 = (the_Source_of G1) . e1 & (the_Target_of G) . e1 = (the_Target_of G1) . e1 ) by A10, Def9;
the_Edges_of G c= the_Edges_of G1 by Def9;
hence e1 in G1 .edgesBetween ((the_Vertices_of G1) \ {v2}) by A10, A11, A12, GLIB_000:31; :: thesis:

end;

then A13: G1 .edgesBetween ((the_Vertices_of G1) \ {v2}) = G .edgesBetween ((the_Vertices_of G) \ {v2}) by TARSKI:2;
A14: the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v2}) by A2, GLIB_000:47
.= the_Edges_of G3 by A13, GLIB_000:47 ;
( dom (the_Source_of G2) = the_Edges_of G2 & dom (the_Target_of G2) = the_Edges_of G2 ) by GLIB_000:4;
then A16: ( dom (the_Source_of G2) = dom (the_Source_of G3) & dom (the_Target_of G2) = dom (the_Target_of G3) ) by A14, GLIB_000:4;
for e1 being object st e1 in dom (the_Source_of G2) holds
(the_Source_of G2) . e1 = (the_Source_of G3) . e1

let e1 be object ; :: thesis:
assume e1 in dom (the_Source_of G2) ; :: thesis:
then A17: e1 in the_Edges_of G2 ;
thus (the_Source_of G2) . e1 = (the_Source_of G1) . e1 by A17, GLIB_000:def 32
.= (the_Source_of G) . e1 by A14, A17, Def9
.= (the_Source_of G3) . e1 by A14, A17, GLIB_000:def 32 ; :: thesis:

end;

then A19: the_Source_of G2 = the_Source_of G3 by A16, FUNCT_1:2;
for e1 being object st e1 in dom (the_Target_of G2) holds
(the_Target_of G2) . e1 = (the_Target_of G3) . e1

let e1 be object ; :: thesis:
assume e1 in dom (the_Target_of G2) ; :: thesis:
then A20: e1 in the_Edges_of G2 ;
thus (the_Target_of G2) . e1 = (the_Target_of G1) . e1 by A20, GLIB_000:def 32
.= (the_Target_of G) . e1 by A14, A20, Def9
.= (the_Target_of G3) . e1 by A14, A20, GLIB_000:def 32 ; :: thesis:

end;

then A22: the_Target_of G2 = the_Target_of G3 by A16, FUNCT_1:2;

the_Vertices_of G c= the_Vertices_of G1 by Def9;
then (the_Vertices_of G) \ {v2} c= (the_Vertices_of G1) \ {v2} by XBOOLE_1:33;
then the_Vertices_of G3 c= (the_Vertices_of G1) \ {v2} by GLIB_000:47;
hence the_Vertices_of G3 c= the_Vertices_of G2 by A2, GLIB_000:47; :: thesis:
thus the_Edges_of G3 c= the_Edges_of G2 by A14; :: thesis:
let e1 be set ; :: thesis:
assume e1 in the_Edges_of G3 ; :: thesis:
thus ( (the_Source_of G3) . e1 = (the_Source_of G2) . e1 & (the_Target_of G3) . e1 = (the_Target_of G2) . e1 ) by A19, A22; :: thesis:

end;

then G2 is Supergraph of G3 by Def9;
hence G2 is addVertex of G3,v1 by A3, A14, A19, A22, Def10; :: thesis: