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 by GLIB_001:def 23; :: thesis: (T .pathBetween a,b) .last() = b
thus (T .pathBetween a,b) .last() = b by A1, GLIB_001:def 23; :: thesis: verum