let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let W be Subset of V; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis:
then consider E being set such that
card V = card E and
( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A2: 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 Def4;
defpred S₁[ object , object ] means $2 Joins $1,v,G1;
A3: for w being object st w in W holds
ex e being object st
( e in G1 .edgesBetween (W,{v}) & S₁[w,e] )

end;

consider f being Function of W,(G1 .edgesBetween (W,{v})) such that
A6: for w being object st w in W holds
S₁[w,f . w] from FUNCT_2:sch 1(A3);
take f ; :: thesis:
A7: ( G1 .edgesBetween (W,{v}) = {} implies W = {} ) by A1, Lm12;
for w1, w2 being object st w1 in W & w2 in W & f . w1 = f . w2 holds
w1 = w2

let w1, w2 be object ; :: thesis:
assume that
A8: ( w1 in W & w2 in W ) and
A9: f . w1 = f . w2 ; :: thesis:
( f . w1 Joins w1,v,G1 & f . w2 Joins w2,v,G1 ) by A6, A8;

end;

end;

let e be object ; :: thesis:
assume A11: e in G1 .edgesBetween (W,{v}) ; :: thesis:
then A12: e SJoins W,{v},G1 by GLIB_000:def 30;
consider w being object such that
A13: ( w in W & e Joins w,v,G1 ) by A12, GLIB_000:102;
consider e1 being object such that
( e1 in E & e1 Joins w,v,G1 ) and
A14: for e2 being object st e2 Joins w,v,G1 holds
e1 = e2 by A2, A13;
( e1 = e & e1 = f . w ) by A13, A14, A6;
hence e in rng f by A13, FUNCT_2:4, A11; :: thesis:

end;