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 Th28;
hence a in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; :: thesis: b in (T .pathBetween (a,b)) .vertices()
(T .pathBetween (a,b)) .last() = b by Th28;
hence b in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; :: thesis: verum