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

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