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
A1: MiddleVertex a,a,b = MiddleVertex a,b,a by Th40;
(T .pathBetween a,b) .first() = a by Th27;
then a in (T .pathBetween a,b) .vertices() by GLIB_001:89;
hence MiddleVertex a,a,b = a by A1, Th45; :: thesis: verum