theorem :: SPRECT_2:63

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 = E-max (L~ f) & E-max (L~ f) <> NE-corner (L~ f) holds
(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2