let f be V22() standard special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies (N-min (L~ f)) .. f < (N-max (L~ f)) .. f )
assume f /. 1 = N-min (L~ f) ; :: thesis: (N-min (L~ f)) .. f < (N-max (L~ f)) .. f
then A1: (N-min (L~ f)) .. f = 1 by FINSEQ_6:43;
A2: N-max (L~ f) in rng f by Th40;
then (N-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A3: (N-max (L~ f)) .. f >= 1 by FINSEQ_3:25;
N-min (L~ f) in rng f by Th39;
then (N-min (L~ f)) .. f <> (N-max (L~ f)) .. f by A2, Th52, FINSEQ_5:9;
hence (N-min (L~ f)) .. f < (N-max (L~ f)) .. f by A3, A1, XXREAL_0:1; :: thesis: verum