theorem Th4: :: HELLY:4

for p being non empty FinSequence holds <*(p . 1)*> is_a_prefix_of p