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