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:128;
( a = (T .pathBetween (a,a)) .first() & (T .walkOf v) .first() = v ) by Th28, GLIB_001:13;
hence (T .pathBetween (a,a)) .vertices() = {a} by A1, GLIB_001:90; :: thesis: verum