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