theorem Th9: :: HELLY:9

for p, q being FinSequence st not p is_a_prefix_of q & not q is_a_prefix_of p holds
p . ((len (maxPrefix (p,q))) + 1) <> q . ((len (maxPrefix (p,q))) + 1)