for p, q being Point of (TOP-REAL 2) st p `1 = q `1 & p `2 = q `2 holds
p = q