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