let n be Nat; :: thesis: for u, p, q, 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
let u, p, q, w be Point of (TOP-REAL n); :: thesis: ( u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| implies u = w )
set r1 = u;
set r2 = w;
assume that
A1: u in halfline (p,q) and
A2: w in halfline (p,q) and
A3: |.(u - p).| = |.(w - p).| ; :: thesis: u = w
A4: n in NAT by ORDINAL1:def 12;

per cases ( p <> q or p = q ) ;

suppose p <> q ; :: thesis: u = w

then A5: |.(q - p).| <> 0 by A4, TOPRNS_1:28;
consider a1 being real number such that
A6: u = ((1 - a1) * p) + (a1 * q) and
A7: a1 >= 0 by A1, A4, TOPREAL9:26;
A8: abs a1 = a1 by A7, ABSVALUE:def 1;
( a1 in REAL & u - p = a1 * (q - p) ) by A6, Lm1, XREAL_0:def 1;
then A9: |.(u - p).| = (abs a1) * |.(q - p).| by A4, TOPRNS_1:7;
consider a2 being real number such that
A10: w = ((1 - a2) * p) + (a2 * q) and
A11: a2 >= 0 by A2, A4, TOPREAL9:26;
( a2 in REAL & w - p = a2 * (q - p) ) by A10, Lm1, XREAL_0:def 1;
then A12: |.(w - p).| = (abs a2) * |.(q - p).| by A4, TOPRNS_1:7;
abs a2 = a2 by A11, ABSVALUE:def 1;
then a1 = a2 by A3, A5, A9, A12, A8, XCMPLX_1:5;
hence u = w by A6, A10; :: thesis: verum

end;

suppose A13: p = q ; :: thesis: u = w

then u in {p} by A1, A4, TOPREAL9:29;
then A14: u = p by TARSKI:def 1;
w in {p} by A2, A4, A13, TOPREAL9:29;
hence u = w by A14, TARSKI:def 1; :: thesis: verum

end;

end;