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 Th31;
then ((T .pathBetween b,c) .vertices() ) /\ ((T .pathBetween c,a) .vertices() ) = {c} by A1, Th38;
then ((T .pathBetween a,b) .vertices() ) /\ (((T .pathBetween b,c) .vertices() ) /\ ((T .pathBetween c,a) .vertices() )) = {c} by A1, ZFMISC_1:52;
hence (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {c} by XBOOLE_1:16; :: thesis: verum