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