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

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