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,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )
let a, b, c be Vertex of T; :: thesis: ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )
set P = T .pathBetween (a,b);
set ci = (T .pathBetween (a,b)) .find c;
set pac = T .pathBetween (a,c);
set pcb = T .pathBetween (c,b);

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

A1: T .pathBetween (a,b) = (T .pathBetween (a,b)) .cut (1,(len (T .pathBetween (a,b)))) by GLIB_001:39;
A2: ( 1 <= (T .pathBetween (a,b)) .find c & 1 = (2 * 0) + 1 ) by ABIAN:12;
assume A3: c in (T .pathBetween (a,b)) .vertices() ; :: thesis: T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b))
then A4: (T .pathBetween (a,b)) .find c <= len (T .pathBetween (a,b)) by GLIB_001:def 19;
A5: (T .pathBetween (a,b)) . ((T .pathBetween (a,b)) .find c) = c by A3, GLIB_001:def 19;
(T .pathBetween (a,b)) . (len (T .pathBetween (a,b))) = (T .pathBetween (a,b)) .last()
.= b by Th28 ;
then A6: T .pathBetween (c,b) = (T .pathBetween (a,b)) .cut (((T .pathBetween (a,b)) .find c),(len (T .pathBetween (a,b)))) by A4, A5, Th35;
(T .pathBetween (a,b)) . 1 = (T .pathBetween (a,b)) .first()
.= a by Th28 ;
then T .pathBetween (a,c) = (T .pathBetween (a,b)) .cut (1,((T .pathBetween (a,b)) .find c)) by A4, A2, A5, Th35;
hence T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A4, A2, A6, A1, GLIB_001:38; :: thesis: verum

end;

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