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,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {(MiddleVertex a,b,c)} by Def3;
A2: (((T .pathBetween a,c) .vertices() ) /\ ((T .pathBetween c,b) .vertices() )) /\ ((T .pathBetween b,a) .vertices() ) = {(MiddleVertex a,c,b)} by Def3;
A3: (T .pathBetween a,b) .vertices() = (T .pathBetween b,a) .vertices() by Th31;
A4: (T .pathBetween b,c) .vertices() = (T .pathBetween c,b) .vertices() by Th31;
(T .pathBetween c,a) .vertices() = (T .pathBetween a,c) .vertices() by Th31;
then {(MiddleVertex a,b,c)} = {(MiddleVertex a,c,b)} by A1, A2, A3, A4, XBOOLE_1:16;
hence MiddleVertex a,b,c = MiddleVertex a,c,b by ZFMISC_1:6; :: thesis: verum