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