:: deftheorem Def2 defines .pathBetween HELLY:def 2 :
for T being _Tree
for a, b being Vertex of T
for b₄ being Path of T holds
( b₄ = T .pathBetween (a,b) iff b₄ is_Walk_from a,b );