let T be _Tree; for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (a,c,b)
let a, b, c be Vertex of T; MiddleVertex (a,b,c) = MiddleVertex (a,c,b)
set PMV1 = MiddleVertex (a,b,c);
set PMV2 = MiddleVertex (a,c,b);
A1:
( (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() & (T .pathBetween (b,c)) .vertices() = (T .pathBetween (c,b)) .vertices() )
by Th32;
A2:
(T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices()
by Th32;
( (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))} & (((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())) /\ ((T .pathBetween (b,a)) .vertices()) = {(MiddleVertex (a,c,b))} )
by Def3;
then
{(MiddleVertex (a,b,c))} = {(MiddleVertex (a,c,b))}
by A1, A2, XBOOLE_1:16;
hence
MiddleVertex (a,b,c) = MiddleVertex (a,c,b)
by ZFMISC_1:3; verum