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

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