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

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