let f be V22() standard special_circular_sequence; :: thesis: N-min (L~ f) <> N-max (L~ f)
(N-min (L~ f)) `1 < (N-max (L~ f)) `1 by Th51;
hence N-min (L~ f) <> N-max (L~ f) ; :: thesis: verum