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:93; :: thesis: verum