let f be non constant standard special_circular_sequence; :: thesis: (E-min (L~ f)) .. f < len f
A1: E-min (L~ f) in rng f by SPRECT_2:49;
len f > 1 by GOBOARD7:36, XXREAL_0:2;
hence (E-min (L~ f)) .. f < len f by A1, Th7; :: thesis: verum