theorem Th1: :: JORDAN5D:1

for n being Nat
for h being FinSequence of (TOP-REAL n) st len h >= 2 holds
h /. (len h) in LSeg (h,((len h) -' 1))