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