let i be Element of NAT ; :: thesis: 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); :: thesis: ( 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
; :: thesis: not LSeg (f /. i),(f /. (i + 2)) c= (LSeg f,i) \/ (LSeg f,(i + 1))
consider p being Point of (TOP-REAL 2) such that
A5:
p in LSeg (f /. i),(f /. (i + 2))
and
A6:
( p `1 <> (f /. i) `1 & p `1 <> (f /. (i + 2)) `1 & p `2 <> (f /. i) `2 & p `2 <> (f /. (i + 2)) `2 )
by A2, A3, A4, Lm5;
set p0 = f /. (i + 1);
i + 1 <= i + 2
by XREAL_1:8;
then
i + 1 <= len f
by A4, XXREAL_0:2;
then A7:
LSeg f,i = LSeg (f /. i),(f /. (i + 1))
by A3, TOPREAL1:def 5;
A8:
1 <= i + 1
by NAT_1:11;
i + (1 + 1) = (i + 1) + 1
;
then A9:
LSeg f,(i + 1) = LSeg (f /. (i + 1)),(f /. (i + 2))
by A4, A8, TOPREAL1:def 5;
assume A10:
LSeg (f /. i),(f /. (i + 2)) c= (LSeg f,i) \/ (LSeg f,(i + 1))
; :: thesis: contradiction