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*>;
A2: len <*p,q*> = 1 + 1 by FINSEQ_1:61;
let i be Nat; :: according to TOPREAL1:def 7 :: 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
A3: 1 <= i and
A4: 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 )
i <= 1 by A2, A4, XREAL_1:8;
then i = 1 by A3, XXREAL_0:1;
then ( <*p,q*> /. i = p & <*p,q*> /. (i + 1) = q ) by FINSEQ_4:26;
hence ( (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 ) by A1; :: thesis: verum