let f be constant standard special_circular_sequence; :: thesis: S-min (L~ f) <> S-max (L~ f)
(S-min (L~ f)) `1 < (S-max (L~ f)) `1 by Th55;
hence S-min (L~ f) <> S-max (L~ f) ; :: thesis: verum