let T be _Tree; :: thesis: for a, b, c being Vertex of T st c in (T .pathBetween a,b) .vertices() holds
MiddleVertex a,b,c = c
let a, b, c be Vertex of T; :: thesis: ( c in (T .pathBetween a,b) .vertices() implies MiddleVertex a,b,c = c )
assume c in (T .pathBetween a,b) .vertices() ; :: thesis: MiddleVertex a,b,c = c
then (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {c} by Lm1;
hence MiddleVertex a,b,c = c by Def3; :: thesis: verum