let n be Nat; :: thesis: 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
let p, q, u, 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

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

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

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

end;

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

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

end;

end;