let T be _Tree; :: thesis: for a, b being Vertex of T holds MiddleVertex a,a,b = a
let a, b be Vertex of T; :: thesis: MiddleVertex a,a,b = a
(T .pathBetween a,b) .first() = a by Th28;
then A1: a in (T .pathBetween a,b) .vertices() by GLIB_001:89;
MiddleVertex a,a,b = MiddleVertex a,b,a by Th41;
hence MiddleVertex a,a,b = a by A1, Th46; :: thesis: verum