let i be 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
f /. (i + 1) is_extremal_in (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 f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) )
assume that
A1: ( f is special & f is alternating ) and
A2: 1 <= i and
A3: i + 2 <= len f ; :: thesis: f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1)))
set p2 = f /. (i + 1);
i + 1 <= i + 2 by XREAL_1:6;
then i + 1 <= len f by A3, XXREAL_0:2;
then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, TOPREAL1:def 3;
then f /. (i + 1) in LSeg (f,i) by RLTOPSP1:68;
then A4: f /. (i + 1) in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) by XBOOLE_0:def 3;
for p, q being Point of (TOP-REAL 2) st f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds
f /. (i + 1) = q by A1, A2, A3, Th35;
hence f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) by A4; :: thesis: verum