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