theorem
for
T being
_Tree 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)))