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

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