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

now :: thesis: for x being object st x in G1 .reachableFrom v1 holds
x in (G2 .reachableFrom w) \/ {v}

let x be object ; :: thesis: ( x in G1 .reachableFrom v1 implies b₁ in (G2 .reachableFrom w) \/ {v} )
assume x in G1 .reachableFrom v1 ; :: thesis: b₁ in (G2 .reachableFrom w) \/ {v}
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 ( ( the Path of W1 is trivial & x <> v ) or not the Path of W1 is trivial or x = v ) ;

suppose A8: ( the Path of W1 is trivial & x <> v ) ; :: thesis: b₁ in (G2 .reachableFrom w) \/ {v}

the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} 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:146;
P2 is_Walk_from w,x by A1, A6, GLIB_001:19;
then x in G2 .reachableFrom w by GLIB_002:def 5;
hence x in (G2 .reachableFrom w) \/ {v} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose the Path of W1 is trivial ; :: thesis: b₁ in (G2 .reachableFrom w) \/ {v}

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

end;

suppose x = v ; :: thesis: b₁ in (G2 .reachableFrom w) \/ {v}

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

end;

end;

end;

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