let T be _Tree; :: thesis: for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c}
let a, b, c be Vertex of T; :: thesis: ( c in (T .pathBetween (a,b)) .vertices() implies (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} )
assume A1: c in (T .pathBetween (a,b)) .vertices() ; :: thesis: (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c}
set P1 = T .pathBetween (a,b);
set P2 = T .pathBetween (b,c);
set P3 = T .pathBetween (c,a);
(T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() by Th32;
then ((T .pathBetween (b,c)) .vertices()) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by A1, Th39;
then ((T .pathBetween (a,b)) .vertices()) /\ (((T .pathBetween (b,c)) .vertices()) /\ ((T .pathBetween (c,a)) .vertices())) = {c} by A1, ZFMISC_1:46;
hence (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by XBOOLE_1:16; :: thesis: verum