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