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 ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds
( p2 `2 = p3 `2 & p1 `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 ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds
( p2 `2 = p3 `2 & p1 `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 ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) implies ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) )
assume that
A1: f is special and
A2: ( f is alternating & 1 <= i ) and
A3: i + 2 <= len f and
A4: p1 = f /. i and
A5: p2 = f /. (i + 1) and
A6: p3 = f /. (i + 2) ; :: thesis: ( ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) or ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) )
( 1 <= i + 1 & i + (1 + 1) = (i + 1) + 1 ) by NAT_1:11;
then ( p2 `1 = p3 `1 or p2 `2 = p3 `2 ) by A1, A3, A5, A6;
hence ( ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) or ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) ) by A2, A3, A4, A6; :: thesis: verum