let T be _Tree; :: thesis: for a, b being Vertex of T holds MiddleVertex (a,b,b) = b
let a, b be Vertex of T; :: thesis: MiddleVertex (a,b,b) = b
MiddleVertex (a,b,b) = MiddleVertex (b,a,b) by Th42;
hence MiddleVertex (a,b,b) = b by Th49; :: thesis: verum