for n being Nat
for p, q, u, w being Point of (TOP-REAL n) st u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| holds
u = w