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() )

assume A1: c in (T .pathBetween a,b) .vertices() ; :: thesis: T .pathBetween a,b = (T .pathBetween a,c) .append (T .pathBetween c,b)
A2: 1 <= (T .pathBetween a,b) .find c by HEYTING3:1;
A3: (T .pathBetween a,b) .find c <= len (T .pathBetween a,b) by A1, GLIB_001:def 19;
A4: 1 = (2 * 0 ) + 1 ;
A5: (T .pathBetween a,b) . 1 = (T .pathBetween a,b) .first()
.= a by Th27 ;
A6: (T .pathBetween a,b) . ((T .pathBetween a,b) .find c) = c by A1, GLIB_001:def 19;
A7: (T .pathBetween a,b) . (len (T .pathBetween a,b)) = (T .pathBetween a,b) .last()
.= b by Th27 ;
A8: T .pathBetween a,c = (T .pathBetween a,b) .cut 1,((T .pathBetween a,b) .find c) by A2, A3, A4, A5, A6, Th34;
A9: T .pathBetween c,b = (T .pathBetween a,b) .cut ((T .pathBetween a,b) .find c),(len (T .pathBetween a,b)) by A3, A6, A7, Th34;
T .pathBetween a,b = (T .pathBetween a,b) .cut 1,(len (T .pathBetween a,b)) by GLIB_001:40;
hence T .pathBetween a,b = (T .pathBetween a,c) .append (T .pathBetween c,b) by A2, A3, A4, A8, A9, GLIB_001:39; :: thesis: verum

end;

assume A10: T .pathBetween a,b = (T .pathBetween a,c) .append (T .pathBetween c,b) ; :: thesis: c in (T .pathBetween a,b) .vertices()
A11: c in (T .pathBetween a,c) .vertices() by Th28;
(T .pathBetween a,c) .vertices() c= (T .pathBetween a,b) .vertices() by A10, Th13, Th15;
hence c in (T .pathBetween a,b) .vertices() by A11; :: thesis: verum