theorem Th3: :: HELLY:3
for p, q being FinSequence holds len (maxPrefix (p,q)) <= len p