let i be Nat; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2)
for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds
( p1 `2 = p2 `2 & p3 `2 <> p2 `2 )
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds
( p1 `2 = p2 `2 & p3 `2 <> p2 `2 )
let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) implies ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) )
assume that
A1: f is special and
A2: f is alternating and
A3: 1 <= i and
A4: i + 2 <= len f and
A5: p1 = f /. i and
A6: p2 = f /. (i + 1) and
A7: p3 = f /. (i + 2) ; :: thesis: ( ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) or ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) )
i + 1 <= i + 2 by XREAL_1:6;
then i + 1 <= len f by A4, XXREAL_0:2;
then ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) by A1, A3, A5, A6;
hence ( ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) or ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) ) by A2, A3, A4, A5, A7; :: thesis: verum