for T being _Tree
for a, b being Vertex of T
for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds
(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t