let G1 be _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: ( v0 is endvertex & v1 = v2 & v1 in G1 .reachableFrom v0 ) ; :: thesis:
then A2: not G1 is _trivial by Th16;
then A3: the_Vertices_of G2 = (the_Vertices_of G1) \ {v0} by GLIB_000:47;
for w being object holds
( w in G2 .reachableFrom v2 iff ( w in G1 .reachableFrom v1 & not w in {v0} ) )

let w be object ; :: thesis:
thus ( w in G2 .reachableFrom v2 implies ( w in G1 .reachableFrom v1 & not w in {v0} ) ) by A1, A3, GLIB_002:14, TARSKI:def 3, XBOOLE_0:def 5; :: thesis:
assume A4: ( w in G1 .reachableFrom v1 & not w in {v0} ) ; :: thesis:
then consider W being Walk of G1 such that
A5: W is_Walk_from v1,w by GLIB_002:def 5;
set P = the Path of W;
( v1 is set & w is set ) by TARSKI:1;
then A6: the Path of W is_Walk_from v1,w by A5, GLIB_001:160;
not v0 in the Path of W .vertices()

assume v0 in the Path of W .vertices() ; :: thesis:

per cases by A1, GLIB_001:143;

suppose v0 = the Path of W .first() ; :: thesis:

then v0 = v2 by A1, A6, GLIB_001:def 23;
then not v0 in {v0} by A3, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

suppose v0 = the Path of W .last() ; :: thesis:

then v0 = w by A6, GLIB_001:def 23;
hence contradiction by A4, TARSKI:def 1; :: thesis:

end;

end;

end;

then reconsider P = the Path of W as Walk of G2 by A2, GLIB_001:171;
P is_Walk_from v2,w by A1, A6, GLIB_001:19;
hence w in G2 .reachableFrom v2 by GLIB_002:def 5; :: thesis:

end;

hence G2 .reachableFrom v2 = (G1 .reachableFrom v1) \ {v0} by XBOOLE_0:def 5; :: thesis: