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)))
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))) ; :: thesis: 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))) ; :: thesis: contradiction

A14: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68;
( 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; :: thesis: verum

end;

suppose A15: p in LSeg ((f /. (i + 1)),(f /. (i + 2))) ; :: thesis: contradiction

A16: f /. (i + 2) in LSeg ((f /. (i + 1)),(f /. (i + 2))) by RLTOPSP1:68;
( 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; :: thesis: verum

end;

end;