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 and
A2: P2 = T .pathBetween a,c and
A3: not b in P2 .vertices() and
A4: not c in P1 .vertices() ; :: thesis: MiddleVertex a,b,c = P1 . (len (maxPrefix P1,P2))
A5: not P1 c= P2 by A1, A2, A3, Th36;
A6: not P2 c= P1 by A1, A2, A4, Th36;
A7: (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {(MiddleVertex a,b,c)} by Def3;
(((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {(P1 . (len (maxPrefix P1,P2)))} by A1, A2, A5, A6, Lm2;
hence MiddleVertex a,b,c = P1 . (len (maxPrefix P1,P2)) by A7, ZFMISC_1:6; :: thesis: verum