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 :: thesis: not P4 c= P3

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