theorem Th39: :: JORDAN4:39

for f being constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 < i2 & i2 + 1 <= len f holds
mid (f,i1,i2) is being_S-Seq