let T be _Tree; :: thesis: for a, b, c being Vertex of T holds
( c in (T .pathBetween a,b) .vertices() iff T .pathBetween a,c is_a_prefix_of T .pathBetween a,b )
let a, b, c be Vertex of T; :: thesis: ( c in (T .pathBetween a,b) .vertices() iff T .pathBetween a,c is_a_prefix_of T .pathBetween a,b )

hereby :: thesis: ( T .pathBetween a,c is_a_prefix_of T .pathBetween a,b implies c in (T .pathBetween a,b) .vertices() )

assume c in (T .pathBetween a,b) .vertices() ; :: thesis: T .pathBetween a,c c= T .pathBetween a,b
then T .pathBetween a,b = (T .pathBetween a,c) .append (T .pathBetween c,b) by Th36;
hence T .pathBetween a,c c= T .pathBetween a,b by Th15; :: thesis: verum

end;

assume T .pathBetween a,c c= T .pathBetween a,b ; :: thesis: c in (T .pathBetween a,b) .vertices()
then A1: (T .pathBetween a,c) .vertices() c= (T .pathBetween a,b) .vertices() by Th13;
c in (T .pathBetween a,c) .vertices() by Th29;
hence c in (T .pathBetween a,b) .vertices() by A1; :: thesis: verum