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:40;
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:39; :: 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