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
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:8;
then i + 1 <= len f by A3, XXREAL_0:2;
then LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A2, TOPREAL1:def 5;
then f /. (i + 1) in LSeg f,i by RLTOPSP1:69;
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, Th58;
hence f /. (i + 1) is_extremal_in (LSeg f,i) \/ (LSeg f,(i + 1)) by A4, Def1; :: thesis: verum