let f be non constant standard special_circular_sequence; :: thesis: ( f /. 1 = E-max (L~ f) implies (E-max (L~ f)) .. f < (E-min (L~ f)) .. f )
A1: E-min (L~ f) in rng f by SPRECT_2:49;
E-max (L~ f) in rng f by SPRECT_2:50;
then A2: (E-min (L~ f)) .. f <> (E-max (L~ f)) .. f by A1, FINSEQ_5:10, SPRECT_2:58;
(E-min (L~ f)) .. f in dom f by A1, FINSEQ_4:30;
then A3: (E-min (L~ f)) .. f >= 1 by FINSEQ_3:27;
assume f /. 1 = E-max (L~ f) ; :: thesis: (E-max (L~ f)) .. f < (E-min (L~ f)) .. f
then (E-max (L~ f)) .. f = 1 by FINSEQ_6:47;
hence (E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A2, A3, XXREAL_0:1; :: thesis: verum