let f be constant standard special_circular_sequence; :: thesis: W-min (L~ f) <> W-max (L~ f)
(W-min (L~ f)) `2 < (W-max (L~ f)) `2 by Th57;
hence W-min (L~ f) <> W-max (L~ f) ; :: thesis: verum