theorem Th33: :: JORDAN4:33

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 <= i2 & i1 > i2 & i1 < len f holds
(mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2