let T be _Tree; :: thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,a,b)
let a, b, c be Vertex of T; :: 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