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};
set P3 = T .pathBetween c,a;
set P2 = T .pathBetween b,c;
set P1 = T .pathBetween a,b;

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;
set i = len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c));
(T .pathBetween a,b) .last() = b by Th28;
then A3: b in (T .pathBetween a,b) .vertices() by GLIB_001:89;
(T .pathBetween a,c) .last() = c by Th28;
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 A4: not T .pathBetween a,c c= T .pathBetween a,b by Th13;
(T .pathBetween a,b) .first() = a by Th28;
then A5: (T .pathBetween a,b) .first() = (T .pathBetween a,c) .first() by Th28;
then reconsider i9 = len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c)) as odd Element of NAT by Th22;
set x = (T .pathBetween a,b) . i9;
(T .pathBetween c,a) .vertices() = (T .pathBetween a,c) .vertices() by Th32;
then A6: not (T .pathBetween a,b) .vertices() c= (T .pathBetween a,c) .vertices() by A2, A3;
then ( len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c)) <= (len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c))) + 2 & (len (maxPrefix (T .pathBetween a,b),(T .pathBetween a,c))) + 2 <= len (T .pathBetween a,b) ) by A5, Th13, Th23, NAT_1:11;
then reconsider x = (T .pathBetween a,b) . i9 as Vertex of T by GLIB_001:8, XXREAL_0:2;
take x ; :: thesis:
not T .pathBetween a,b c= T .pathBetween a,c by A6, Th13;
hence (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {x} by A4, Lm2; :: thesis:

end;

end;