let G1 be non _trivial simple _Graph; :: thesis:
let v be Vertex of G1; :: thesis:
let G2 be removeVertex of G1,v; :: thesis:
A1: G1 is Supergraph of G2 by GLIB_006:57;
A2: the_Vertices_of G2 = (the_Vertices_of G1) \ {v} by GLIB_000:47;
A3: the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:47
.= (G1 .edgesBetween (the_Vertices_of G1)) \ (v .edgesInOut()) by Th1
.= (the_Edges_of G1) \ (v .edgesInOut()) by GLIB_000:34 ;
v in {v} by TARSKI:def 1;
then A4: not v in the_Vertices_of G2 by A2, XBOOLE_0:def 5;
for x being object st x in v .allNeighbors() holds
x in the_Vertices_of G2

proof

let x be object ; :: thesis:
assume A5: x in v .allNeighbors() ; :: thesis:
x <> v

proof

assume x = v ; :: thesis:
then consider e being object such that
A6: e Joins v,v,G1 by A5, GLIB_000:71;
thus contradiction by A6, GLIB_000:18; :: thesis:

end;

then not x in {v} by TARSKI:def 1;
hence x in the_Vertices_of G2 by A2, A5, XBOOLE_0:def 5; :: thesis:

end;

then A7: v .allNeighbors() c= the_Vertices_of G2 by TARSKI:def 3;

now :: thesis:

thus the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A2, ZFMISC_1:116; :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
thus not e Joins v,v,G1 by GLIB_000:18; :: thesis:
let v1 be object ; :: thesis:

hereby :: thesis:

assume A8: not v1 in v .allNeighbors() ; :: thesis:
v1 is set by TARSKI:1;
hence not e Joins v1,v,G1 by A8, GLIB_000:71, GLIB_000:14; :: thesis:

end;

let v2 be object ; :: thesis:
assume A9: ( v1 <> v & v2 <> v & e DJoins v1,v2,G1 ) ; :: thesis:
thus e DJoins v1,v2,G2 :: thesis:

proof

assume not e DJoins v1,v2,G2 ; :: thesis:
then A10: not e in the_Edges_of G2 by A1, A9, GLIB_006:71;
e in the_Edges_of G1 by A9, GLIB_000:def 14;
then e in v .edgesInOut() by A3, A10, XBOOLE_0:def 5;

per cases ) . e = v or (the_Target_of G1) . e = v ) by GLIB_000:61;

suppose (the_Source_of G1) . e = v ; :: thesis:

hence contradiction by A9, GLIB_000:def 14; :: thesis:

end;

suppose (the_Target_of G1) . e = v ; :: thesis:

hence contradiction by A9, GLIB_000:def 14; :: thesis:

end;

end;

end;

end;

reconsider E = v .edgesInOut() as set ;
take E = E; :: thesis:
card E = v .degree() by GLIB_000:19;
hence card (v .allNeighbors()) = card E by Th5; :: thesis:
E /\ (the_Edges_of G2) = {}

proof

assume E /\ (the_Edges_of G2) <> {} ; :: thesis:
then consider e being object such that
A11: e in E /\ (the_Edges_of G2) by XBOOLE_0:def 1;
A12: ( e in E & e in the_Edges_of G2 ) by A11, XBOOLE_0:def 4;
then ( (the_Source_of G1) . e = v or (the_Target_of G1) . e = v ) by GLIB_000:61;
then ( (the_Source_of G2) . e = v or (the_Target_of G2) . e = v ) by A12, GLIB_000:def 32;
then ( (the_Source_of G2) . e in {v} or (the_Target_of G2) . e in {v} ) by TARSKI:def 1;
then ( not (the_Source_of G2) . e in the_Vertices_of G2 or not (the_Target_of G2) . e in the_Vertices_of G2 ) by A2, XBOOLE_0:def 5;
hence contradiction by A12, FUNCT_2:5; :: thesis:

end;

hence E misses the_Edges_of G2 by XBOOLE_0:def 7; :: thesis:
A13: (the_Edges_of G2) \/ E c= the_Edges_of G1 by XBOOLE_1:8;
for e being object st e in the_Edges_of G1 holds
e in (the_Edges_of G2) \/ E

proof

let e be object ; :: thesis:
assume A14: e in the_Edges_of G1 ; :: thesis:
( e in the_Edges_of G2 or e in E ) by A3, A14, XBOOLE_0:def 5;
hence e in (the_Edges_of G2) \/ E by XBOOLE_0:def 3; :: thesis:

end;

then the_Edges_of G1 c= (the_Edges_of G2) \/ E by TARSKI:def 3;
hence the_Edges_of G1 = (the_Edges_of G2) \/ E by A13, XBOOLE_0:def 10; :: thesis:
let v1 be object ; :: thesis:
assume A15: v1 in v .allNeighbors() ; :: thesis:
then consider e1 being object such that
A16: e1 Joins v,v1,G1 by GLIB_000:71;
take e1 = e1; :: thesis:
( v1 in the_Vertices_of G1 & e1 is set ) by A15, TARSKI:1;
hence e1 in E by A16, GLIB_000:64; :: thesis:
thus A17: e1 Joins v1,v,G1 by A16, GLIB_000:14; :: thesis:
let e2 be object ; :: thesis:
assume e2 Joins v1,v,G1 ; :: thesis:
hence e1 = e2 by A17, GLIB_000:def 20; :: thesis:

end;

hence G1 is addAdjVertexAll of G2,v,v .allNeighbors() by A1, A4, A7, GLIB_007:def 4; :: thesis: