let i be Nat; for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds
not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1)))
let f be FinSequence of the carrier of (TOP-REAL 2); ( f is special & f is alternating & 1 <= i & i + 2 <= len f implies not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) )
set p1 = f /. i;
set p2 = f /. (i + 2);
assume that
A1:
f is special
and
A2:
f is alternating
and
A3:
1 <= i
and
A4:
i + 2 <= len f
; not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1)))
set p0 = f /. (i + 1);
i + 1 <= i + 2
by XREAL_1:6;
then
i + 1 <= len f
by A4, XXREAL_0:2;
then A5:
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1)))
by A3, TOPREAL1:def 3;
( 1 <= i + 1 & i + (1 + 1) = (i + 1) + 1 )
by NAT_1:11;
then A6:
LSeg (f,(i + 1)) = LSeg ((f /. (i + 1)),(f /. (i + 2)))
by A4, TOPREAL1:def 3;
consider p being Point of (TOP-REAL 2) such that
A7:
p in LSeg ((f /. i),(f /. (i + 2)))
and
A8:
p `1 <> (f /. i) `1
and
A9:
p `1 <> (f /. (i + 2)) `1
and
A10:
p `2 <> (f /. i) `2
and
A11:
p `2 <> (f /. (i + 2)) `2
by A2, A3, A4, Lm5;
assume A12:
LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1)))
; contradiction