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