theorem Th67: :: SPRECT_2:67

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 /. i = W-min (L~ f) & W-min (L~ f) <> SW-corner (L~ f) holds
<*(SW-corner (L~ f))*> ^ (mid (f,i,j)) is S-Sequence_in_R2