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:6; :: thesis: verum