theorem Th27: :: TOPREAL8:27

for f being circular unfolded s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds
(LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)}