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