let T be _Tree; :: thesis: for a being Vertex of T holds MiddleVertex a,a,a = a
let a be Vertex of T; :: thesis: MiddleVertex a,a,a = a
a in {a} by TARSKI:def 1;
then a in (T .pathBetween a,a) .vertices() by Th29;
hence MiddleVertex a,a,a = a by Th45; :: thesis: verum