let T be _Tree; :: thesis:
let a, b, c be Vertex of T; :: thesis:
let P1, P4 be Path of T; :: thesis:
assume that
A1: P1 = T .pathBetween (a,b) and
A2: P4 = T .pathBetween (a,c) and
A3: not P1 c= P4 and
A4: not P4 c= P1 ; :: thesis:
set P3 = T .pathBetween (c,a);
A5: (T .pathBetween (c,a)) .vertices() = P4 .vertices() by A2, Th32;
set i = len (maxPrefix (P1,P4));
P1 .first() = a by A1, Th28;
then A6: P1 .first() = P4 .first() by A2, Th28;
then reconsider i9 = len (maxPrefix (P1,P4)) as odd Element of NAT by Th22;
set x = P1 . i9;
A7: len (maxPrefix (P1,P4)) <= (len (maxPrefix (P1,P4))) + 2 by NAT_1:11;

A8: now :: thesis:

assume b in (T .pathBetween (c,a)) .vertices() ; :: thesis:
then b in P4 .vertices() by A2, Th32;
then P4 = (T .pathBetween (a,b)) .append (T .pathBetween (b,c)) by A2, Th36;
hence contradiction by A1, A3, Th15; :: thesis:

end;

proof

end;

A41: (P4 .cut (i9,(len P4))) .last() = c by A19, Th28;
then A42: ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) is_Walk_from b,c by A12, A20, A16, GLIB_001:30;

now :: thesis:

assume c in P1 .vertices() ; :: thesis:
then P1 = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A1, Th36;
hence contradiction by A2, A4, Th15; :: thesis:

end;

then x <> c by A11, GLIB_001:87;
then A43: P4 .cut (i9,(len P4)) is open by A20, A41;
not ((P1 .cut (i9,(len P1))) .reverse()) .first() in (P4 .cut (i9,(len P4))) .vertices() by A8, A5, A23, A16;
then ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) is Path of T by A12, A20, A18, A43, A22, A24, Th18;
then ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) = T .pathBetween (b,c) by A42, Def2;
then A44: x in (T .pathBetween (b,c)) .vertices() by A21, A13, GLIB_001:87;
A45: x in P4 .vertices() by A9, A17, GLIB_001:87;
A46: ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) c= {x}

proof

set Pcx = T .pathBetween (c,x);
set Pxa = T .pathBetween (x,a);
set Pbx = T .pathBetween (b,x);
set Pxc = T .pathBetween (x,c);
set Pax = T .pathBetween (a,x);
set Pxb = T .pathBetween (x,b);
let z be object ; :: according to TARSKI:def 3 :: thesis:
A47: (T .pathBetween (b,x)) .vertices() = (T .pathBetween (x,b)) .vertices() by Th32;
A48: (T .pathBetween (c,x)) .vertices() = (T .pathBetween (x,c)) .vertices() by Th32;
A49: (T .pathBetween (c,x)) .last() = x by Th28
.= (T .pathBetween (x,a)) .first() by Th28 ;
T .pathBetween (c,a) = (T .pathBetween (c,x)) .append (T .pathBetween (x,a)) by A5, A45, Th36;
then A50: (T .pathBetween (c,a)) .vertices() = ((T .pathBetween (c,x)) .vertices()) \/ ((T .pathBetween (x,a)) .vertices()) by A49, GLIB_001:93;
A51: (T .pathBetween (b,x)) .last() = x by Th28
.= (T .pathBetween (x,c)) .first() by Th28 ;
T .pathBetween (b,c) = (T .pathBetween (b,x)) .append (T .pathBetween (x,c)) by A44, Th36;
then A52: (T .pathBetween (b,c)) .vertices() = ((T .pathBetween (b,x)) .vertices()) \/ ((T .pathBetween (x,c)) .vertices()) by A51, GLIB_001:93;
A53: (T .pathBetween (a,x)) .last() = x by Th28
.= (T .pathBetween (x,b)) .first() by Th28 ;
P1 = (T .pathBetween (a,x)) .append (T .pathBetween (x,b)) by A1, A14, Th36;
then A54: P1 .vertices() = ((T .pathBetween (a,x)) .vertices()) \/ ((T .pathBetween (x,b)) .vertices()) by A53, GLIB_001:93;
assume A55: z in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) ; :: thesis:
then A56: z in (P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by XBOOLE_0:def 4;
then z in P1 .vertices() by XBOOLE_0:def 4;
then A57: ( z in (T .pathBetween (a,x)) .vertices() or z in (T .pathBetween (x,b)) .vertices() ) by A54, XBOOLE_0:def 3;
z in (T .pathBetween (c,a)) .vertices() by A55, XBOOLE_0:def 4;
then A58: ( z in (T .pathBetween (c,x)) .vertices() or z in (T .pathBetween (x,a)) .vertices() ) by A50, XBOOLE_0:def 3;
z in (T .pathBetween (b,c)) .vertices() by A56, XBOOLE_0:def 4;
then A59: ( z in (T .pathBetween (b,x)) .vertices() or z in (T .pathBetween (x,c)) .vertices() ) by A52, XBOOLE_0:def 3;

per cases by A57, A59, A58, Th32;

suppose ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (b,x)) .vertices() ) ; :: thesis:

then z in ((T .pathBetween (a,x)) .vertices()) /\ ((T .pathBetween (x,b)) .vertices()) by A47, XBOOLE_0:def 4;
hence z in {x} by A1, A14, Th39; :: thesis:

end;

suppose ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ; :: thesis:

then z in ((T .pathBetween (a,x)) .vertices()) /\ ((T .pathBetween (x,c)) .vertices()) by A48, XBOOLE_0:def 4;
hence z in {x} by A2, A45, Th39; :: thesis:

end;

suppose ( z in (T .pathBetween (b,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ; :: thesis:

then z in ((T .pathBetween (b,x)) .vertices()) /\ ((T .pathBetween (x,c)) .vertices()) by A48, XBOOLE_0:def 4;
hence z in {x} by A44, Th39; :: thesis:

end;

x in (P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by A14, A44, XBOOLE_0:def 4;
then x in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by A5, A45, XBOOLE_0:def 4;
then {x} c= ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by ZFMISC_1:31;
hence ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} by A46; :: thesis: