let f be non trivial special unfolded standard FinSequence of (TOP-REAL 2); :: thesis: ( ( ( f /. 1 <> S-min (L~ f) & f /. (len f) <> S-min (L~ f) ) or ( f /. 1 <> S-max (L~ f) & f /. (len f) <> S-max (L~ f) ) ) implies S-min (L~ f) <> S-max (L~ f) )
assume ( ( f /. 1 <> S-min (L~ f) & f /. (len f) <> S-min (L~ f) ) or ( f /. 1 <> S-max (L~ f) & f /. (len f) <> S-max (L~ f) ) ) ; :: thesis: S-min (L~ f) <> S-max (L~ f)
then (S-min (L~ f)) `1 < (S-max (L~ f)) `1 by Th10;
hence S-min (L~ f) <> S-max (L~ f) ; :: thesis: verum