let T be _Tree; :: thesis: 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; :: thesis: 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; :: thesis: verum