theorem Th64: :: SPRECT_2:64

for f being constant standard special_circular_sequence
for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds
(mid (f,i,j)) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2