theorem :: SPRECT_5:45

for f being constant standard special_circular_sequence st f /. 1 = N-max (L~ f) & N-max (L~ f) <> E-max (L~ f) holds
(N-max (L~ f)) .. f < (E-max (L~ f)) .. f