let G2 be _Graph; 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 ; 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; 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; 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; ( 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 )
; 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 for x being object st x in G1 .reachableFrom v1 holds
x in (G2 .reachableFrom w) \/ {v}let x be
object ;
( x in G1 .reachableFrom v1 implies b1 in (G2 .reachableFrom w) \/ {v} )assume
x in G1 .reachableFrom v1
;
b1 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 V5() & x <> v ) or not the Path of W1 is V5() or x = v )
;
suppose A8:
( the
Path of
W1 is
V5() &
x <> v )
;
b1 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;
verum 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; verum