let T be _Tree; :: thesis: for a, b, c being Vertex of T holds MiddleVertex a,b,c = MiddleVertex b,c,a
let a, b, c be Vertex of T; :: thesis: MiddleVertex a,b,c = MiddleVertex b,c,a
thus MiddleVertex a,b,c = MiddleVertex b,a,c by Th42
.= MiddleVertex b,c,a by Th41 ; :: thesis: verum