let G be _Graph; :: thesis: for e, x, y being set

for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds

y in G .reachableDFrom v1

let e, x, y be set ; :: thesis: for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds

y in G .reachableDFrom v1

let v1 be Vertex of G; :: thesis: ( x in G .reachableDFrom v1 & e DJoins x,y,G implies y in G .reachableDFrom v1 )

set RFV = G .reachableDFrom v1;

assume that

A1: x in G .reachableDFrom v1 and

A2: e DJoins x,y,G ; :: thesis: y in G .reachableDFrom v1

consider W being directed Walk of G such that

A3: W is_Walk_from v1,x by A1, Def6;

( W .addEdge e is directed & W .addEdge e is_Walk_from v1,y ) by A2, A3, GLIB_001:123;

hence y in G .reachableDFrom v1 by Def6; :: thesis: verum

for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds

y in G .reachableDFrom v1

let e, x, y be set ; :: thesis: for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds

y in G .reachableDFrom v1

let v1 be Vertex of G; :: thesis: ( x in G .reachableDFrom v1 & e DJoins x,y,G implies y in G .reachableDFrom v1 )

set RFV = G .reachableDFrom v1;

assume that

A1: x in G .reachableDFrom v1 and

A2: e DJoins x,y,G ; :: thesis: y in G .reachableDFrom v1

consider W being directed Walk of G such that

A3: W is_Walk_from v1,x by A1, Def6;

( W .addEdge e is directed & W .addEdge e is_Walk_from v1,y ) by A2, A3, GLIB_001:123;

hence y in G .reachableDFrom v1 by Def6; :: thesis: verum