let T be _Tree; :: thesis: for a, b being Vertex of T holds (T .pathBetween a,b) .reverse() = T .pathBetween b,a
let a, b be Vertex of T; :: thesis: (T .pathBetween a,b) .reverse() = T .pathBetween b,a
set P = T .pathBetween a,b;
set R = T .pathBetween b,a;
T .pathBetween a,b is_Walk_from a,b by Def2;
then (T .pathBetween a,b) .reverse() is_Walk_from b,a by GLIB_001:24;
hence (T .pathBetween a,b) .reverse() = T .pathBetween b,a by Def2; :: thesis: verum