let T be _Tree; :: thesis:
let a, b, c be Vertex of T; :: thesis:
set Pac = T .pathBetween a,c;
set Pcb = T .pathBetween c,b;
set Pab = T .pathBetween a,b;
thus ( c in (T .pathBetween a,b) .vertices() implies ((T .pathBetween a,c) .vertices() ) /\ ((T .pathBetween c,b) .vertices() ) = {c} ) :: thesis:

assume A1: c in (T .pathBetween a,b) .vertices() ; :: thesis:
thus ((T .pathBetween a,c) .vertices() ) /\ ((T .pathBetween c,b) .vertices() ) c= {c} :: according to XBOOLE_0:def 10 :: thesis:

per cases ;

suppose T .pathBetween a,b is trivial ; :: thesis:

then (T .pathBetween a,b) .first() = (T .pathBetween a,b) .last() by GLIB_001:128;
then A8: (T .pathBetween a,b) .vertices() = {a} by A3, A4, Th29;
x in ((T .pathBetween a,c) .vertices() ) \/ ((T .pathBetween c,b) .vertices() ) by A2, XBOOLE_0:def 3;
then x in (T .pathBetween a,b) .vertices() by A5, A6, A7, GLIB_001:94;
hence x in {c} by A1, A8, TARSKI:def 1; :: thesis:

end;

suppose A9: not T .pathBetween a,b is trivial ; :: thesis:

consider m being odd Element of NAT such that
A10: m <= len (T .pathBetween a,c) and
A11: (T .pathBetween a,c) . m = x by A2, GLIB_001:88;
1 <= m by HEYTING3:1;
then m in dom (T .pathBetween a,c) by A10, FINSEQ_3:27;
then A12: (T .pathBetween a,b) . m = x by A5, A11, GLIB_001:33;
consider n being odd Element of NAT such that
A13: n <= len (T .pathBetween c,b) and
A14: (T .pathBetween c,b) . n = x by A2, GLIB_001:88;
1 <= n by HEYTING3:1;
then 1 - 1 <= n - 1 by XREAL_1:11;
then reconsider n1 = n - 1 as even Element of NAT by INT_1:16;
A15: n1 + 1 = n ;
then n1 < len (T .pathBetween c,b) by A13, NAT_1:13;
then A16: (T .pathBetween a,b) . ((len (T .pathBetween a,c)) + n1) = x by A5, A6, A7, A14, A15, GLIB_001:34;
(len (T .pathBetween a,c)) + (n1 + 1) <= (len (T .pathBetween a,c)) + (len (T .pathBetween c,b)) by A13, XREAL_1:8;
then (((len (T .pathBetween a,c)) + n1) + 1) - 1 <= ((len (T .pathBetween a,c)) + (len (T .pathBetween c,b))) - 1 by XREAL_1:11;
then A17: (((len (T .pathBetween a,c)) + n1) + 1) - 1 <= ((len (T .pathBetween a,b)) + 1) - 1 by A5, A6, A7, GLIB_001:29;
A18: m <= (len (T .pathBetween a,c)) + n1 by A10, NAT_1:12;

per cases by A18, XXREAL_0:1;

suppose A19: m < (len (T .pathBetween a,c)) + n1 ; :: thesis:

then (T .pathBetween a,b) .first() = x by A12, A16, A17, GLIB_001:def 28
.= (T .pathBetween a,b) .last() by A12, A16, A17, A19, GLIB_001:def 28 ;
then T .pathBetween a,b is closed by GLIB_001:def 24;
hence x in {c} by A9; :: thesis:

end;

suppose A20: m = (len (T .pathBetween a,c)) + n1 ; :: thesis:

then n1 = 0 by A10, NAT_1:16;
hence x in {c} by A6, A11, A20, TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {c} ; :: thesis:
then x = c by TARSKI:def 1;
then ( x = (T .pathBetween a,c) .last() & x = (T .pathBetween c,b) .first() ) by Th27;
then ( x in (T .pathBetween a,c) .vertices() & x in (T .pathBetween c,b) .vertices() ) by GLIB_001:89;
hence x in ((T .pathBetween a,c) .vertices() ) /\ ((T .pathBetween c,b) .vertices() ) by XBOOLE_0:def 4; :: thesis:

end;