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;
set RFV = G .reachableFrom v;
let x be set ; :: 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 x' = x as Vertex of G ;
consider W being directed Walk of G such that
A2: W is_Walk_from v,x' by A1, Def6;
thus x in G .reachableFrom v by A2, Def5; :: thesis: verum