let G be _Graph; :: thesis: for v1 being Vertex of G
for e, x, y being set st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
let v1 be Vertex of G; :: thesis: for e, x, y being set st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
let e, x, y be set ; :: thesis: ( x in G .reachableFrom v1 & e Joins x,y,G implies y in G .reachableFrom v1 )
set RFV = G .reachableFrom v1;
assume A1: ( x in G .reachableFrom v1 & e Joins x,y,G ) ; :: thesis: y in G .reachableFrom v1
then consider W being Walk of G such that
A2: W is_Walk_from v1,x by Def5;
W .addEdge e is_Walk_from v1,y by A1, A2, GLIB_001:67;
hence y in G .reachableFrom v1 by Def5; :: thesis: verum