let G2 be _Graph; :: thesis:
let v be Vertex of G2; :: thesis:
let e, w be object ; :: thesis:
let G1 be addAdjVertex of G2,v,e,w; :: thesis:
let v1 be Vertex of G1; :: thesis:
assume A1: ( v1 = v & not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) ; :: thesis:
G2 is Subgraph of G1 by GLIB_006:57;
then A2: G2 .reachableFrom v c= G1 .reachableFrom v1 by A1, GLIB_002:14;
A3: e Joins v1,w,G1 by A1, GLIB_006:131;
v1 in G1 .reachableFrom v1 by GLIB_002:9;
then {w} c= G1 .reachableFrom v1 by A3, GLIB_002:10, ZFMISC_1:31;
then A4: (G2 .reachableFrom v) \/ {w} c= G1 .reachableFrom v1 by A2, XBOOLE_1:8;

now :: thesis:

let x be object ; :: thesis:
assume x in G1 .reachableFrom v1 ; :: thesis:
then consider W1 being Walk of G1 such that
A5: W1 is_Walk_from v1,x by GLIB_002:def 5;
set P1 = the Path of W1;
x is set by TARSKI:1;
then A6: the Path of W1 is_Walk_from v1,x by A5, GLIB_001:160;
then A7: ( the Path of W1 .first() = v1 & the Path of W1 .last() = x ) by GLIB_001:def 23;

per cases ;

suppose A8: ( the Path of W1 is trivial & x <> w ) ; :: thesis:

the_Vertices_of G1 = (the_Vertices_of G2) \/ {w} by A1, GLIB_006:def 12;
then x in the_Vertices_of G2 by A7, A8, ZFMISC_1:136;
then not e in the Path of W1 .edges() by A1, A7, GLIB_006:147;
then reconsider P2 = the Path of W1 as Walk of G2 by A1, A8, GLIB_006:145;
P2 is_Walk_from v,x by A1, A6, GLIB_001:19;
then x in G2 .reachableFrom v by GLIB_002:def 5;
hence x in (G2 .reachableFrom v) \/ {w} by XBOOLE_0:def 3; :: thesis:

end;

suppose the Path of W1 is trivial ; :: thesis:

then x = v1 by A7, GLIB_001:127;
then x in G2 .reachableFrom v by A1, GLIB_002:9;
hence x in (G2 .reachableFrom v) \/ {w} by XBOOLE_0:def 3; :: thesis:

end;

suppose x = w ; :: thesis:

then x in {w} by TARSKI:def 1;
hence x in (G2 .reachableFrom v) \/ {w} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then G1 .reachableFrom v1 c= (G2 .reachableFrom v) \/ {w} by TARSKI:def 3;
hence G1 .reachableFrom v1 = (G2 .reachableFrom v) \/ {w} by A4, XBOOLE_0:def 10; :: thesis: