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 Th30;
hence MiddleVertex (a,a,a) = a by Th46; :: thesis: verum