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

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