theorem Th42: :: HELLY:42

for T being _Tree
for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,a,c)