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 and
A2: f is alternating and
A3: 1 <= i and
A4: i + 2 <= len f ; :: thesis: f /. (i + 1) is_extremal_in (LSeg f,i) \/ (LSeg f,(i + 1))
i + 1 <= i + 2 by XREAL_1:8;
then A5: i + 1 <= len f by A4, XXREAL_0:2;
set p2 = f /. (i + 1);
A6: 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, A4, Th58;
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A3, A5, TOPREAL1:def 5;
then f /. (i + 1) in LSeg f,i by TOPREAL1:6;
then f /. (i + 1) in (LSeg f,i) \/ (LSeg f,(i + 1)) by XBOOLE_0:def 3;
hence f /. (i + 1) is_extremal_in (LSeg f,i) \/ (LSeg f,(i + 1)) by A6, Def1; :: thesis: verum