let f be V22() standard special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies (N-min (L~ f)) .. f < (E-max (L~ f)) .. f )
A1: N-min (L~ f) in rng f by Th39;
assume f /. 1 = N-min (L~ f) ; :: thesis: (N-min (L~ f)) .. f < (E-max (L~ f)) .. f
then A2: (N-min (L~ f)) .. f = 1 by FINSEQ_6:43;
(N-max (L~ f)) `1 <= (NE-corner (L~ f)) `1 by PSCOMP_1:38;
then (N-max (L~ f)) `1 <= E-bound (L~ f) by EUCLID:52;
then (N-min (L~ f)) `1 < E-bound (L~ f) by Th51, XXREAL_0:2;
then A3: (N-min (L~ f)) `1 < (E-max (L~ f)) `1 by EUCLID:52;
A4: E-max (L~ f) in rng f by Th46;
then (E-max (L~ f)) .. f >= 1 by FINSEQ_4:21;
hence (N-min (L~ f)) .. f < (E-max (L~ f)) .. f by A4, A1, A3, A2, FINSEQ_5:9, XXREAL_0:1; :: thesis: verum