let G1 be non _trivial _Graph; :: thesis:
let v0, v1 be Vertex of G1; :: thesis:
let G2 be removeVertex of G1,v0; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 = v2 & not v1 in G1 .reachableFrom v0 ) ; :: thesis:
then A2: G2 .reachableFrom v2 c= G1 .reachableFrom v1 by GLIB_002:14;
for w being object st w in G1 .reachableFrom v1 holds
w in G2 .reachableFrom v2

let w be object ; :: thesis:
assume w in G1 .reachableFrom v1 ; :: thesis:
then consider W being Walk of G1 such that
A3: W is_Walk_from v1,w by GLIB_002:def 5;
not v0 in W .vertices()

assume A4: v0 in W .vertices() ; :: thesis:
reconsider m = 1 as odd Element of NAT by POLYFORM:4;
reconsider n = W .find v0 as odd Element of NAT ;
set U = W .cut (m,n);
( m <= n & n <= len W ) by A4, GLIB_001:def 19, CHORD:2;
then W .cut (m,n) is_Walk_from W . m,W . n by GLIB_001:37;
then W .cut (m,n) is_Walk_from W .first() ,W . n by GLIB_001:def 6;
then W .cut (m,n) is_Walk_from v1,W . n by A3, GLIB_001:def 23;
then W .cut (m,n) is_Walk_from v1,v0 by A4, GLIB_001:def 19;
then (W .cut (m,n)) .reverse() is_Walk_from v0,v1 by GLIB_001:23;
hence contradiction by A1, GLIB_002:def 5; :: thesis:

end;

then reconsider W2 = W as Walk of G2 by GLIB_001:171;
W2 is_Walk_from v2,w by A1, A3, GLIB_001:19;
hence w in G2 .reachableFrom v2 by GLIB_002:def 5; :: thesis:

end;

then G1 .reachableFrom v1 c= G2 .reachableFrom v2 by TARSKI:def 3;
hence G2 .reachableFrom v2 = G1 .reachableFrom v1 by A2, XBOOLE_0:def 10; :: thesis: