let n be Element of NAT ; :: thesis: for p, q, r being Point of (TOP-REAL n) st q in LSeg p,r & r in LSeg p,q holds
q = r
let p, q, r be Point of (TOP-REAL n); :: thesis: ( q in LSeg p,r & r in LSeg p,q implies q = r )
assume q in LSeg p,r ; :: thesis: ( not r in LSeg p,q or q = r )
then consider r1 being Real such that
A1: q = ((1 - r1) * p) + (r1 * r) and
A2: 0 <= r1 and
A3: r1 <= 1 ;
assume r in LSeg p,q ; :: thesis: q = r
then consider r2 being Real such that
A4: r = ((1 - r2) * p) + (r2 * q) and
0 <= r2 and
A5: r2 <= 1 ;
A6: r1 * r2 <= 1 by A2, A3, A5, XREAL_1:162;
A7: (1 - r2) + (r2 * (1 - r1)) = 1 - (r2 * r1) ;
A8: r = ((1 - r2) * p) + ((r2 * ((1 - r1) * p)) + (r2 * (r1 * r))) by A1, A4, EUCLID:36
.= (((1 - r2) * p) + (r2 * ((1 - r1) * p))) + (r2 * (r1 * r)) by EUCLID:30
.= (((1 - r2) * p) + ((r2 * (1 - r1)) * p)) + (r2 * (r1 * r)) by EUCLID:34
.= ((1 - (r2 * r1)) * p) + (r2 * (r1 * r)) by A7, EUCLID:37
.= ((1 - (r2 * r1)) * p) + ((r2 * r1) * r) by EUCLID:34 ;
A9: (1 - r1) + (r1 * (1 - r2)) = 1 - (r1 * r2) ;
A10: q = ((1 - r1) * p) + ((r1 * ((1 - r2) * p)) + (r1 * (r2 * q))) by A1, A4, EUCLID:36
.= (((1 - r1) * p) + (r1 * ((1 - r2) * p))) + (r1 * (r2 * q)) by EUCLID:30
.= (((1 - r1) * p) + ((r1 * (1 - r2)) * p)) + (r1 * (r2 * q)) by EUCLID:34
.= ((1 - (r1 * r2)) * p) + (r1 * (r2 * q)) by A9, EUCLID:37
.= ((1 - (r1 * r2)) * p) + ((r1 * r2) * q) by EUCLID:34 ;

per cases ( r1 * r2 = 1 or r1 * r2 < 1 ) by A6, XXREAL_0:1;

suppose A11: r1 * r2 = 1 ; :: thesis: q = r

then ( 1 <= r1 or 1 <= r2 ) by A2, XREAL_1:164;
then ( 1 * r1 = 1 or 1 * r2 = 1 ) by A3, A5, XXREAL_0:1;
hence q = (0 * p) + r by A1, A11, EUCLID:33
.= (0. (TOP-REAL n)) + r by EUCLID:33
.= r by EUCLID:31 ;
:: thesis: verum

end;

suppose A12: r1 * r2 < 1 ; :: thesis: q = r

hence q = p by A10, Th14
.= r by A8, A12, Th14 ;
:: thesis: verum

end;

end;