let G2 be _Graph; :: thesis:
let v, v1 be object ; :: thesis:
let G1 be addAdjVertexAll of G2,v,{v1}; :: thesis:
assume A1: ( v1 in the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis:
then A2: {v1} c= the_Vertices_of G2 by ZFMISC_1:31;
then A3: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, Def4;
consider E being set such that
A4: ( card {v1} = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A5: for v2 being object st v2 in {v1} holds
ex e1 being object st
( e1 in E & e1 Joins v2,v,G1 & ( for e2 being object st e2 Joins v2,v,G1 holds
e1 = e2 ) ) by A1, A2, Def4;
v1 in {v1} by TARSKI:def 1;
then consider e1 being object such that
A6: ( e1 in E & e1 Joins v1,v,G1 ) and
for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 by A5;
take e1 ; :: thesis:
E /\ (the_Edges_of G2) = {} by A4, XBOOLE_0:def 7;
hence A7: not e1 in the_Edges_of G2 by A6, Lm7; :: thesis:
consider e being object such that
A8: E = {e} by A4, CARD_1:29;
A9: E = {e1} by A6, A8, TARSKI:def 1;
then A10: the_Edges_of G1 = (the_Edges_of G2) \/ {e1} by A4;
consider f, g being Function of E,({v1} \/ {v}) such that
A11: the_Source_of G1 = (the_Source_of G2) +* f and
A12: the_Target_of G1 = (the_Target_of G2) +* g and
A13: for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) by A1, A2, A4, Th52;
reconsider f = f, g = g as Function of {e1},{v1,v} by A9, ENUMSET1:1;
A14: e1 DJoins f . e1,g . e1,G1 by A6, A13;

per cases by A6, GLIB_000:16;

suppose e1 DJoins v1,v,G1 ; :: thesis:

then ( (the_Source_of G1) . e1 = v1 & (the_Target_of G1) . e1 = v ) by GLIB_000:def 14;
then A15: ( v1 = f . e1 & v = g . e1 ) by A14, GLIB_000:def 14;
for z being object st z in dom f holds
f . z = v1 by A15, TARSKI:def 1;
then f = (dom f) --> v1 by FUNCOP_1:11;
then f = {e1} --> v1 by FUNCT_2:def 1;
then A16: the_Source_of G1 = (the_Source_of G2) +* (e1 .--> v1) by A11, FUNCOP_1:def 9;
for z being object st z in dom g holds
g . z = v by A15, TARSKI:def 1;
then g = (dom g) --> v by FUNCOP_1:11;
then g = {e1} --> v by FUNCT_2:def 1;
then g = e1 .--> v by FUNCOP_1:def 9;
hence ( G1 is addAdjVertex of G2,v,e1,v1 or G1 is addAdjVertex of G2,v1,e1,v ) by A1, A7, A3, A10, A16, GLIB_006:def 12, A12; :: thesis:

end;

suppose e1 DJoins v,v1,G1 ; :: thesis:

then ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 = v1 ) by GLIB_000:def 14;
then A17: ( v = f . e1 & v1 = g . e1 ) by A14, GLIB_000:def 14;
for z being object st z in dom f holds
f . z = v by A17, TARSKI:def 1;
then f = (dom f) --> v by FUNCOP_1:11;
then f = {e1} --> v by FUNCT_2:def 1;
then A18: the_Source_of G1 = (the_Source_of G2) +* (e1 .--> v) by A11, FUNCOP_1:def 9;
for z being object st z in dom g holds
g . z = v1 by A17, TARSKI:def 1;
then g = (dom g) --> v1 by FUNCOP_1:11;
then g = {e1} --> v1 by FUNCT_2:def 1;
then g = e1 .--> v1 by FUNCOP_1:def 9;
hence ( G1 is addAdjVertex of G2,v,e1,v1 or G1 is addAdjVertex of G2,v1,e1,v ) by A1, A7, A3, A10, A18, GLIB_006:def 12, A12; :: thesis:

end;