:: deftheorem Def3 defines MiddleVertex HELLY:def 3 :
for T being _Tree
for a, b, c, b₅ being Vertex of T holds
( b₅ = MiddleVertex (a,b,c) iff (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₅} );