let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: for i being Nat
for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds
ex p being Point of (TOP-REAL 2) st
( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )
let i be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds
ex p being Point of (TOP-REAL 2) st
( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) implies ex p being Point of (TOP-REAL 2) st
( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) )
assume ( f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) ) ; :: thesis: ex p being Point of (TOP-REAL 2) st
( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )
then ( p1 `1 <> p2 `1 & p1 `2 <> p2 `2 ) ;
hence ex p being Point of (TOP-REAL 2) st
( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) by Th14; :: thesis: verum