let T be _Tree; for P1, P2 being Path of T
for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds
MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))
let P1, P2 be Path of T; for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds
MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))
let a, b, c be Vertex of T; ( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() implies MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) )
assume that
A1:
( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) )
and
A2:
( not b in P2 .vertices() & not c in P1 .vertices() )
; MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))
( not P1 c= P2 & not P2 c= P1 )
by A1, A2, Th37;
then A3:
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P2))))}
by A1, Lm2;
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))}
by Def3;
hence
MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))
by A3, ZFMISC_1:3; verum