theorem :: SPRECT_5:59
for f being constant standard special_circular_sequence st f /. 1 = S-min (L~ f) & S-min (L~ f) <> W-min (L~ f) holds
(S-min (L~ f)) .. f < (W-min (L~ f)) .. f