let i be Element of 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:8;
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 5;
( 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 5;
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
per cases
( p in LSeg (f /. i),(f /. (i + 1)) or p in LSeg (f /. (i + 1)),(f /. (i + 2)) )
by A7, A5, A6, A12, XBOOLE_0:def 3;
suppose A13:
p in LSeg (f /. i),
(f /. (i + 1))
;
contradictionA14:
f /. i in LSeg (f /. i),
(f /. (i + 1))
by RLTOPSP1:69;
(
LSeg (f /. i),
(f /. (i + 1)) is
vertical or
LSeg (f /. i),
(f /. (i + 1)) is
horizontal )
by A1, A5, Th41;
hence
contradiction
by A8, A10, A13, A14, Def2, Def3;
verum end; suppose A15:
p in LSeg (f /. (i + 1)),
(f /. (i + 2))
;
contradictionA16:
f /. (i + 2) in LSeg (f /. (i + 1)),
(f /. (i + 2))
by RLTOPSP1:69;
(
LSeg (f /. (i + 1)),
(f /. (i + 2)) is
vertical or
LSeg (f /. (i + 1)),
(f /. (i + 2)) is
horizontal )
by A1, A6, Th41;
hence
contradiction
by A9, A11, A15, A16, Def2, Def3;
verum end;