let G be _Graph; :: thesis: for v1 being Vertex of G
for e, x, y being object 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 object st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
let e, x, y be object ; :: thesis: ( x in G .reachableFrom v1 & e Joins x,y,G implies y in G .reachableFrom v1 )
set RFV = G .reachableFrom v1;
assume that
A1: x in G .reachableFrom v1 and
A2: e Joins x,y,G ; :: thesis: y in G .reachableFrom v1
consider W being Walk of G such that
A3: W is_Walk_from v1,x by A1, Def5;
W .addEdge e is_Walk_from v1,y by A2, A3, GLIB_001:66;
hence y in G .reachableFrom v1 by Def5; :: thesis: verum