let G be _Graph; :: thesis: for v being Vertex of G holds v in G .reachableDFrom v
let v be Vertex of G; :: thesis: v in G .reachableDFrom v
G .walkOf v is_Walk_from v,v by GLIB_001:13;
hence v in G .reachableDFrom v by Def6; :: thesis: verum