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

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