let T be _Tree; :: thesis: for a, b being Vertex of T holds
( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )
let a, b be Vertex of T; :: thesis: ( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )
A1: T .pathBetween (a,b) is_Walk_from a,b by Def2;
hence (T .pathBetween (a,b)) .first() = a ; :: thesis: (T .pathBetween (a,b)) .last() = b
thus (T .pathBetween (a,b)) .last() = b by A1; :: thesis: verum