let T be _Tree; :: thesis: 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; :: thesis: 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; :: thesis: ( 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() ) ; :: thesis: 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; :: thesis: verum