let p be Point of (TOP-REAL 2); :: thesis: <*p*> is special
set f = <*p*>;
let i be Nat; :: according to TOPREAL1:def 7 :: thesis: ( not 1 <= i or not i + 1 <= len <*p*> or (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 )
assume that
A1: 1 <= i and
A2: i + 1 <= len <*p*> ; :: thesis: ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 )
len <*p*> = 0 + 1 by FINSEQ_1:56;
hence ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 ) by A1, A2, XREAL_1:8; :: thesis: verum