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