let T be _Tree; :: thesis: for a, b, c being Vertex of T holds MiddleVertex a,b,c = MiddleVertex b,a,c
let a, b, c be Vertex of T; :: thesis: MiddleVertex a,b,c = MiddleVertex b,a,c
set PMV1 = MiddleVertex a,b,c;
set PMV2 = MiddleVertex b,a,c;
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 b,a) .vertices() ) /\ ((T .pathBetween a,c) .vertices() )) /\ ((T .pathBetween c,b) .vertices() ) = {(MiddleVertex b,a,c)} ) by Def3;
then {(MiddleVertex a,b,c)} = {(MiddleVertex b,a,c)} by A1, A2, XBOOLE_1:16;
hence MiddleVertex a,b,c = MiddleVertex b,a,c by ZFMISC_1:6; :: thesis: verum