set P1 = T .pathBetween a,b;
set P2 = T .pathBetween b,c;
set P3 = T .pathBetween c,a;
defpred S₁[ Vertex of T, Vertex of T, Vertex of T, Vertex of T] means (((T .pathBetween $1,$2) .vertices() ) /\ ((T .pathBetween $2,$3) .vertices() )) /\ ((T .pathBetween $3,$1) .vertices() ) = {$4};

per cases ;

suppose A1: ( c in (T .pathBetween a,b) .vertices() or a in (T .pathBetween b,c) .vertices() or b in (T .pathBetween c,a) .vertices() ) ; :: thesis:

per cases by A1;

suppose c in (T .pathBetween a,b) .vertices() ; :: thesis:

then S₁[a,b,c,c] by Lm1;
hence ex b₁ being Vertex of T st (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {b₁} ; :: thesis:

end;

suppose a in (T .pathBetween b,c) .vertices() ; :: thesis:

then S₁[b,c,a,a] by Lm1;
hence ex b₁ being Vertex of T st (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {b₁} by XBOOLE_1:16; :: thesis:

end;

suppose b in (T .pathBetween c,a) .vertices() ; :: thesis:

then S₁[c,a,b,b] by Lm1;
hence ex b₁ being Vertex of T st (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {b₁} by XBOOLE_1:16; :: thesis:

end;

end;

end;

suppose A2: ( not c in (T .pathBetween a,b) .vertices() & not a in (T .pathBetween b,c) .vertices() & not b in (T .pathBetween c,a) .vertices() ) ; :: thesis:

set P4 = T .pathBetween a,c;
A3: (T .pathBetween c,a) .vertices() = (T .pathBetween a,c) .vertices() by Th31;
(T .pathBetween a,b) .first() = a by Th27;
then A4: (T .pathBetween a,b) .first() = (T .pathBetween a,c) .first() by Th27;
(T .pathBetween a,b) .last() = b by Th27;
then b in (T .pathBetween a,b) .vertices() by GLIB_001:89;
then A5: not (T .pathBetween a,b) .vertices() c= (T .pathBetween a,c) .vertices() by A2, A3;
then A6: not T .pathBetween a,b c= T .pathBetween a,c by Th13;
(T .pathBetween a,c) .last() = c by Th27;
then c in (T .pathBetween a,c) .vertices() by GLIB_001:89;
then not (T .pathBetween a,c) .vertices() c= (T .pathBetween a,b) .vertices() by A2;
then A7: not T .pathBetween a,c c= T .pathBetween a,b by Th13;
set i = len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c));
reconsider i' = len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c)) as odd Element of NAT by A4, Th21;
A8: len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c)) <= (len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c))) + 2 by NAT_1:11;
A9: (len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c))) + 2 <= len (T .pathBetween a,b) by A4, A5, Th13, Th22;
set x = (T .pathBetween a,b) . i';
reconsider x = (T .pathBetween a,b) . i' as Vertex of T by A8, A9, GLIB_001:8, XXREAL_0:2;
take x ; :: thesis:
thus (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {x} by A6, A7, Lm2; :: thesis:

end;

end;