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 ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() or ( not c in (T .pathBetween (a,b)) .vertices() & not a in (T .pathBetween (b,c)) .vertices() & not b in (T .pathBetween (c,a)) .vertices() ) ) ;

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: ex b₁ being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₁}

per cases ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() ) by A1;

suppose c in (T .pathBetween (a,b)) .vertices() ; :: thesis: ex b₁ being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₁}

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: verum

end;

suppose a in (T .pathBetween (b,c)) .vertices() ; :: thesis: ex b₁ being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₁}

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: verum

end;

suppose b in (T .pathBetween (c,a)) .vertices() ; :: thesis: ex b₁ being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₁}

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: verum

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: ex b₁ being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₁}

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:88;
(T .pathBetween (a,c)) .last() = c by Th28;
then c in (T .pathBetween (a,c)) .vertices() by GLIB_001:88;
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:7, XXREAL_0:2;
take x ; :: thesis: (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {x}
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: verum

end;

end;