let T be _Tree; :: thesis: for a being Vertex of T holds T .pathBetween (a,a) = T .walkOf a
let a be Vertex of T; :: thesis: T .pathBetween (a,a) = T .walkOf a
consider b being Vertex of T such that
A1: T .pathBetween (a,a) = T .walkOf b by GLIB_001:128;
{a} = (T .pathBetween (a,a)) .vertices() by HELLY:30
.= {b} by A1, GLIB_001:90 ;
hence T .pathBetween (a,a) = T .walkOf a by A1, ZFMISC_1:3; :: thesis: verum