let i be Element of 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 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: ( ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) or ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) )
A8: 1 <= i + 1 by NAT_1:11;
i + (1 + 1) = (i + 1) + 1 ;
then ( p2 `1 = p3 `1 or p2 `2 = p3 `2 ) by A1, A4, A6, A7, A8, TOPREAL1:def 7;
hence ( ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) or ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) ) by A2, A3, A4, A5, A7, Def4; :: thesis: verum