let G1, G2 be _Graph; :: thesis: for G being GraphUnion of G1,G2
for v2 being Vertex of G2
for v being Vertex of G st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 & v = v2 holds
G .reachableFrom v = G2 .reachableFrom v2
let G be GraphUnion of G1,G2; :: thesis: for v2 being Vertex of G2
for v being Vertex of G st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 & v = v2 holds
G .reachableFrom v = G2 .reachableFrom v2
let v2 be Vertex of G2; :: thesis: for v being Vertex of G st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 & v = v2 holds
G .reachableFrom v = G2 .reachableFrom v2
let v be Vertex of G; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 & v = v2 implies G .reachableFrom v = G2 .reachableFrom v2 )
assume that
A1: G1 tolerates G2 and
A2: ( the_Vertices_of G1 misses the_Vertices_of G2 & v = v2 ) ; :: thesis: G .reachableFrom v = G2 .reachableFrom v2
G is Supergraph of G2 by A1, GLIB_014:26;
then G2 is Subgraph of G by GLIB_006:57;
then A3: G2 .reachableFrom v2 c= G .reachableFrom v by A2, GLIB_002:14;
now :: thesis: for y being object st y in G .reachableFrom v holds
y in G2 .reachableFrom v2
let y be object ; :: thesis: ( y in G .reachableFrom v implies y in G2 .reachableFrom v2 )
assume y in G .reachableFrom v ; :: thesis: y in G2 .reachableFrom v2
then consider W being Walk of G such that
A4: W is_Walk_from v,y by GLIB_002:def 5;
now :: thesis: W is not Walk of G1
assume W is Walk of G1 ; :: thesis: contradiction
then reconsider W1 = W as Walk of G1 ;
W .first() = v2 by A2, A4, GLIB_001:def 23;
then v2 in W .vertices() by GLIB_001:88;
then v2 in W1 .vertices() by GLIB_001:98;
hence contradiction by A2, XBOOLE_0:3; :: thesis: verum
end;
then reconsider W2 = W as Walk of G2 by A1, A2, Th126;
W2 is_Walk_from v2,y by A2, A4, GLIB_001:19;
hence y in G2 .reachableFrom v2 by GLIB_002:def 5; :: thesis: verum
end;
then G .reachableFrom v c= G2 .reachableFrom v2 by TARSKI:def 3;
hence G .reachableFrom v = G2 .reachableFrom v2 by A3, XBOOLE_0:def 10; :: thesis: verum