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:6; :: thesis: verum