for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds
<*p,q*> is being_S-Seq by FINSEQ_3:94, FINSEQ_1:44, Lm2, Lm6, Th38;