let T be _Tree; :: thesis: for a, b being Vertex of T holds
( a in (T .pathBetween a,b) .vertices() & b in (T .pathBetween a,b) .vertices() )
let a, b be Vertex of T; :: thesis: ( a in (T .pathBetween a,b) .vertices() & b in (T .pathBetween a,b) .vertices() )
(T .pathBetween a,b) .first() = a by Th27;
hence a in (T .pathBetween a,b) .vertices() by GLIB_001:89; :: thesis: b in (T .pathBetween a,b) .vertices()
(T .pathBetween a,b) .last() = b by Th27;
hence b in (T .pathBetween a,b) .vertices() by GLIB_001:89; :: thesis: verum