let T be _Tree; 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; ( 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; 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; verum