let G be _Graph; :: thesis: for v being Vertex of G holds G .reachableDFrom v c= G .reachableFrom v

let v be Vertex of G; :: thesis: G .reachableDFrom v c= G .reachableFrom v

set RFD = G .reachableDFrom v;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G .reachableDFrom v or x in G .reachableFrom v )

assume A1: x in G .reachableDFrom v ; :: thesis: x in G .reachableFrom v

then reconsider x9 = x as Vertex of G ;

ex W being directed Walk of G st W is_Walk_from v,x9 by A1, Def6;

hence x in G .reachableFrom v by Def5; :: thesis: verum

let v be Vertex of G; :: thesis: G .reachableDFrom v c= G .reachableFrom v

set RFD = G .reachableDFrom v;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G .reachableDFrom v or x in G .reachableFrom v )

assume A1: x in G .reachableDFrom v ; :: thesis: x in G .reachableFrom v

then reconsider x9 = x as Vertex of G ;

ex W being directed Walk of G st W is_Walk_from v,x9 by A1, Def6;

hence x in G .reachableFrom v by Def5; :: thesis: verum