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);
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:23;
hence (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) by Def2; :: thesis: verum