theorem Th3: :: HELLY:3

for p, q being FinSequence holds len (maxPrefix (p,q)) <= len p