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