let f be V19() standard special_circular_sequence; :: thesis: (E-min (L~ f)) .. f < len f
( E-min (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:45, XXREAL_0:2;
hence (E-min (L~ f)) .. f < len f by Th7; :: thesis: verum