let T be _Tree; :: thesis: for a, b being Vertex of T holds MiddleVertex a,b,a = a
let a, b be Vertex of T; :: thesis: MiddleVertex a,b,a = a
MiddleVertex a,a,b = MiddleVertex a,b,a by Th41;
hence MiddleVertex a,b,a = a by Th48; :: thesis: verum