let f be V19() standard special_circular_sequence; :: thesis: ( f /. 1 = W-min (L~ f) implies (W-max (L~ f)) .. f > 1 )
assume A1: f /. 1 = W-min (L~ f) ; :: thesis: (W-max (L~ f)) .. f > 1
then (W-min (L~ f)) .. f = 1 by FINSEQ_6:43;
hence (W-max (L~ f)) .. f > 1 by A1, Th21; :: thesis: verum