for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
(1 / 2) * (p1 + p2) <> p1