let T be _Tree; :: thesis: for a being Vertex of T holds (T .pathBetween a,a) .vertices() = {a}
let a be Vertex of T; :: thesis: (T .pathBetween a,a) .vertices() = {a}
set P = T .pathBetween a,a;
consider v being Vertex of T such that
A1: T .pathBetween a,a = T .walkOf v by GLIB_001:129;
( a = (T .pathBetween a,a) .first() & (T .walkOf v) .first() = v ) by Th28, GLIB_001:14;
hence (T .pathBetween a,a) .vertices() = {a} by A1, GLIB_001:91; :: thesis: verum