theorem :: GLIB_008:28

for T being _Tree
for a being Vertex of T holds T .pathBetween (a,a) = T .walkOf a