let T be _Tree; :: thesis: for P1, P2, P3, P4 being Path of T
for a, b, c being Vertex of T st P1 = T .pathBetween a,b & P2 = T .pathBetween a,c & P3 = T .pathBetween b,a & P4 = T .pathBetween b,c & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds
P1 . (len (maxPrefix P1,P2)) = P3 . (len (maxPrefix P3,P4))
let P1, P2, P3, P4 be Path of T; :: thesis: for a, b, c being Vertex of T st P1 = T .pathBetween a,b & P2 = T .pathBetween a,c & P3 = T .pathBetween b,a & P4 = T .pathBetween b,c & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds
P1 . (len (maxPrefix P1,P2)) = P3 . (len (maxPrefix P3,P4))
let a, b, c be Vertex of T; :: thesis: ( P1 = T .pathBetween a,b & P2 = T .pathBetween a,c & P3 = T .pathBetween b,a & P4 = T .pathBetween b,c & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() implies P1 . (len (maxPrefix P1,P2)) = P3 . (len (maxPrefix P3,P4)) )
assume that
A1: P1 = T .pathBetween a,b and
A2: P2 = T .pathBetween a,c and
A3: P3 = T .pathBetween b,a and
A4: P4 = T .pathBetween b,c and
A5: not b in P2 .vertices() and
A6: not c in P1 .vertices() and
A7: not a in P4 .vertices() ; :: thesis: P1 . (len (maxPrefix P1,P2)) = P3 . (len (maxPrefix P3,P4))

now

assume P4 c= P3 ; :: thesis: contradiction
then A8: P4 .vertices() c= P3 .vertices() by Th13;
c in P4 .vertices() by A4, Th29;
then c in P3 .vertices() by A8;
hence contradiction by A1, A3, A6, Th32; :: thesis: verum

end;

then not c in P3 .vertices() by A3, A4, Th37;
then A9: MiddleVertex b,a,c = P3 . (len (maxPrefix P3,P4)) by A3, A4, A7, Th51;
MiddleVertex a,b,c = P1 . (len (maxPrefix P1,P2)) by A1, A2, A5, A6, Th51;
hence P1 . (len (maxPrefix P1,P2)) = P3 . (len (maxPrefix P3,P4)) by A9, Th42; :: thesis: verum