let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
let w be Vertex of G1; :: thesis:
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v = w ) ; :: thesis:
then consider E being set such that
A2: ( card V = card E & E misses the_Edges_of G2 ) and
A3: the_Edges_of G1 = (the_Edges_of G2) \/ E and
A4: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by GLIB_007:def 4;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in w .allNeighbors() ; :: thesis:
then consider e being object such that
A5: e Joins w,x,G1 by GLIB_000:71;
not e in the_Edges_of G2

proof

assume e in the_Edges_of G2 ; :: thesis:
then e Joins w,x,G2 by A5, GLIB_006:72;
hence contradiction by A1, GLIB_000:13; :: thesis:

end;

then ( ( w = v & x in V ) or ( x = v & w in V ) ) by A1, A2, A3, A5, GLIB_007:51;
hence x in V by A1; :: thesis:

end;

assume x in V ; :: thesis:
then consider e1 being object such that
A6: ( e1 in E & e1 Joins x,v,G1 ) and
for e2 being object st e2 Joins x,v,G1 holds
e1 = e2 by A4;
x is set by TARSKI:1;
hence x in w .allNeighbors() by A1, A6, GLIB_000:14, GLIB_000:71; :: thesis:

end;

hence w .allNeighbors() = V by TARSKI:2; :: thesis:

per cases ;

suppose A7: V <> {} ; :: thesis:

V c= V ;
then consider f being Function of V,(G1 .edgesBetween (V,{v})) such that
A8: ( f is one-to-one & f is onto ) and
A9: for u being object st u in V holds
f . u Joins u,v,G1 by A1, GLIB_007:57;
A10: rng f = G1 .edgesBetween (V,{w}) by A1, A8, FUNCT_2:def 3;
the_Vertices_of G2 c= the_Vertices_of G1 by GLIB_006:def 9;
then V c= the_Vertices_of G1 by A1, XBOOLE_1:1;
then A11: G1 .edgesBetween (V,{w}) c= G1 .edgesBetween ((the_Vertices_of G1),{w}) by GLIB_000:37;

now :: thesis:

let e be object ; :: thesis:
assume e in G1 .edgesBetween ((the_Vertices_of G1),{w}) ; :: thesis:
then A12: e SJoins the_Vertices_of G1,{w},G1 by GLIB_000:def 30;
ex u being object st e Joins u,w,G1

proof

per cases ) . e in the_Vertices_of G1 & (the_Target_of G1) . e in {w} ) or ( (the_Target_of G1) . e in the_Vertices_of G1 & (the_Source_of G1) . e in {w} ) ) by A12, GLIB_000:def 15;

suppose A13: ( (the_Source_of G1) . e in the_Vertices_of G1 & (the_Target_of G1) . e in {w} ) ; :: thesis:

take (the_Source_of G1) . e ; :: thesis:
A14: (the_Target_of G1) . e = w by A13, TARSKI:def 1;
e in the_Edges_of G1 by A12, GLIB_000:def 15;
hence e Joins (the_Source_of G1) . e,w,G1 by A14, GLIB_000:def 13; :: thesis:

end;

suppose A15: ( (the_Target_of G1) . e in the_Vertices_of G1 & (the_Source_of G1) . e in {w} ) ; :: thesis:

take (the_Target_of G1) . e ; :: thesis:
A16: (the_Source_of G1) . e = w by A15, TARSKI:def 1;
e in the_Edges_of G1 by A12, GLIB_000:def 15;
hence e Joins (the_Target_of G1) . e,w,G1 by A16, GLIB_000:def 13; :: thesis:

end;

end;

end;

then consider u being object such that
A17: e Joins u,w,G1 ;
( u in V & w in {w} ) by A1, A17, GLIB_007:def 4, TARSKI:def 1;
then e SJoins V,{w},G1 by A17, GLIB_000:17;
hence e in G1 .edgesBetween (V,{w}) by GLIB_000:def 30; :: thesis:

end;

then G1 .edgesBetween ((the_Vertices_of G1),{w}) c= G1 .edgesBetween (V,{w}) by TARSKI:def 3;
then G1 .edgesBetween (V,{w}) = G1 .edgesBetween ((the_Vertices_of G1),{w}) by A11, XBOOLE_0:def 10;
then A18: rng f = w .edgesInOut() by A10, GLIB_000:151;
set u = the Element of V;
A19: ( the Element of V in V & v in {v} ) by A7, TARSKI:def 1;
then f . the Element of V Joins the Element of V,v,G1 by A9;
then f . the Element of V SJoins V,{v},G1 by A19, GLIB_000:17;
then f . the Element of V in G1 .edgesBetween (V,{v}) by GLIB_000:def 30;
then dom f = V by FUNCT_2:def 1;
then A20: card V = card (w .edgesInOut()) by A8, A18, CARD_1:70;
for e being object holds not e Joins w,w,G1 by A1, GLIB_007:def 4;
hence w .degree() = card V by A20, GLIB_000:154; :: thesis:

end;

suppose A21: V = {} ; :: thesis:

then A22: G1 is addVertex of G2,v by GLIB_007:55;
{w} \ (the_Vertices_of G2) = {w} by A1, ZFMISC_1:59;
then w in {v} \ (the_Vertices_of G2) by A1, TARSKI:def 1;
hence w .degree() = card V by A21, A22, GLIB_000:157, GLIB_006:88; :: thesis:

end;

end;