let T be _Tree; :: thesis: for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()
let a, b be Vertex of T; :: thesis: (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()
(T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) by Th31;
hence (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() by GLIB_001:92; :: thesis: verum