let f be non trivial special unfolded standard FinSequence of (TOP-REAL 2); :: thesis: ( ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) implies W-min (L~ f) <> W-max (L~ f) )

assume ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) ; :: thesis: W-min (L~ f) <> W-max (L~ f)

then (W-min (L~ f)) `2 < (W-max (L~ f)) `2 by Th12;

hence W-min (L~ f) <> W-max (L~ f) ; :: thesis: verum

assume ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) ; :: thesis: W-min (L~ f) <> W-max (L~ f)

then (W-min (L~ f)) `2 < (W-max (L~ f)) `2 by Th12;

hence W-min (L~ f) <> W-max (L~ f) ; :: thesis: verum