let p, q be Point of (TOP-REAL 2); :: thesis: ( ( p `1 = q `1 or p `2 = q `2 ) implies <*p,q*> is special )
assume A1: ( p `1 = q `1 or p `2 = q `2 ) ; :: thesis: <*p,q*> is special
set f = <*p,q*>;
let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len <*p,q*> or (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 )
assume that
A2: 1 <= i and
A3: i + 1 <= len <*p,q*> ; :: thesis: ( (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 )
len <*p,q*> = 1 + 1 by FINSEQ_1:44;
then i <= 1 by A3, XREAL_1:6;
then A4: i = 1 by A2, XXREAL_0:1;
then <*p,q*> /. i = p by FINSEQ_4:17;
hence ( (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 ) by A1, A4, FINSEQ_4:17; :: thesis: verum