let T be _Tree; for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a)
let a, b be Vertex of T; (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; verum