ex v being Vertex of G st W = G .walkOf v by GLIB_001:128;
hence ( W .edges() is empty & W .edges() is trivial ) by Th25; :: thesis: verum