theorem Th30: :: HELLY:30

for T being _Tree
for a being Vertex of T holds (T .pathBetween (a,a)) .vertices() = {a}