let G1, G2 be _Graph; :: thesis: for G being GraphUnion of G1,G2
for v1 being Vertex of G1
for v being Vertex of G st the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 holds
G .reachableFrom v = G1 .reachableFrom v1
let G be GraphUnion of G1,G2; :: thesis: for v1 being Vertex of G1
for v being Vertex of G st the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 holds
G .reachableFrom v = G1 .reachableFrom v1
let v1 be Vertex of G1; :: thesis: for v being Vertex of G st the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 holds
G .reachableFrom v = G1 .reachableFrom v1
let v be Vertex of G; :: thesis: ( the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 implies G .reachableFrom v = G1 .reachableFrom v1 )

per cases ( G1 tolerates G2 or not G1 tolerates G2 ) ;

suppose A1: G1 tolerates G2 ; :: thesis: ( the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 implies G .reachableFrom v = G1 .reachableFrom v1 )

assume A2: ( the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 ) ; :: thesis: G .reachableFrom v = G1 .reachableFrom v1
G1 is Subgraph of G by GLIB_006:57;
then A3: G1 .reachableFrom v1 c= G .reachableFrom v by A2, GLIB_002:14;

now :: thesis: for y being object st y in G .reachableFrom v holds
y in G1 .reachableFrom v1

let y be object ; :: thesis: ( y in G .reachableFrom v implies y in G1 .reachableFrom v1 )
assume y in G .reachableFrom v ; :: thesis: y in G1 .reachableFrom v1
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 G2

assume W is Walk of G2 ; :: thesis: contradiction
then reconsider W2 = W as Walk of G2 ;
W .first() = v1 by A2, A4, GLIB_001:def 23;
then v1 in W .vertices() by GLIB_001:88;
then v1 in W2 .vertices() by GLIB_001:98;
hence contradiction by A2, XBOOLE_0:3; :: thesis: verum

end;

then reconsider W1 = W as Walk of G1 by A1, A2, Th126;
W1 is_Walk_from v1,y by A2, A4, GLIB_001:19;
hence y in G1 .reachableFrom v1 by GLIB_002:def 5; :: thesis: verum

end;

then G .reachableFrom v c= G1 .reachableFrom v1 by TARSKI:def 3;
hence G .reachableFrom v = G1 .reachableFrom v1 by A3, XBOOLE_0:def 10; :: thesis: verum

end;

suppose not G1 tolerates G2 ; :: thesis: ( the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 implies G .reachableFrom v = G1 .reachableFrom v1 )

then G1 == G by GLIB_014:def 26;
hence ( the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 implies G .reachableFrom v = G1 .reachableFrom v1 ) by GLIB_002:17; :: thesis: verum

end;

end;