let n be 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:160;

A7: (1 - r2) + (r2 * (1 - r1)) = 1 - (r2 * r1) ;

A8: r = ((1 - r2) * p) + ((r2 * ((1 - r1) * p)) + (r2 * (r1 * r))) by A1, A4, RLVECT_1:def 5

.= (((1 - r2) * p) + (r2 * ((1 - r1) * p))) + (r2 * (r1 * r)) by RLVECT_1:def 3

.= (((1 - r2) * p) + ((r2 * (1 - r1)) * p)) + (r2 * (r1 * r)) by RLVECT_1:def 7

.= ((1 - (r2 * r1)) * p) + (r2 * (r1 * r)) by A7, RLVECT_1:def 6

.= ((1 - (r2 * r1)) * p) + ((r2 * r1) * r) by RLVECT_1:def 7 ;

A9: (1 - r1) + (r1 * (1 - r2)) = 1 - (r1 * r2) ;

A10: q = ((1 - r1) * p) + ((r1 * ((1 - r2) * p)) + (r1 * (r2 * q))) by A1, A4, RLVECT_1:def 5

.= (((1 - r1) * p) + (r1 * ((1 - r2) * p))) + (r1 * (r2 * q)) by RLVECT_1:def 3

.= (((1 - r1) * p) + ((r1 * (1 - r2)) * p)) + (r1 * (r2 * q)) by RLVECT_1:def 7

.= ((1 - (r1 * r2)) * p) + (r1 * (r2 * q)) by A9, RLVECT_1:def 6

.= ((1 - (r1 * r2)) * p) + ((r1 * r2) * q) by RLVECT_1:def 7 ;

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:160;

A7: (1 - r2) + (r2 * (1 - r1)) = 1 - (r2 * r1) ;

A8: r = ((1 - r2) * p) + ((r2 * ((1 - r1) * p)) + (r2 * (r1 * r))) by A1, A4, RLVECT_1:def 5

.= (((1 - r2) * p) + (r2 * ((1 - r1) * p))) + (r2 * (r1 * r)) by RLVECT_1:def 3

.= (((1 - r2) * p) + ((r2 * (1 - r1)) * p)) + (r2 * (r1 * r)) by RLVECT_1:def 7

.= ((1 - (r2 * r1)) * p) + (r2 * (r1 * r)) by A7, RLVECT_1:def 6

.= ((1 - (r2 * r1)) * p) + ((r2 * r1) * r) by RLVECT_1:def 7 ;

A9: (1 - r1) + (r1 * (1 - r2)) = 1 - (r1 * r2) ;

A10: q = ((1 - r1) * p) + ((r1 * ((1 - r2) * p)) + (r1 * (r2 * q))) by A1, A4, RLVECT_1:def 5

.= (((1 - r1) * p) + (r1 * ((1 - r2) * p))) + (r1 * (r2 * q)) by RLVECT_1:def 3

.= (((1 - r1) * p) + ((r1 * (1 - r2)) * p)) + (r1 * (r2 * q)) by RLVECT_1:def 7

.= ((1 - (r1 * r2)) * p) + (r1 * (r2 * q)) by A9, RLVECT_1:def 6

.= ((1 - (r1 * r2)) * p) + ((r1 * r2) * q) by RLVECT_1:def 7 ;

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

end;

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

then
( 1 <= r1 or 1 <= r2 )
by A2, XREAL_1:162;

then ( 1 * r1 = 1 or 1 * r2 = 1 ) by A3, A5, XXREAL_0:1;

hence q = (0 * p) + r by A1, A11, RLVECT_1:def 8

.= (0. (TOP-REAL n)) + r by RLVECT_1:10

.= r by RLVECT_1:4 ;

:: thesis: verum

end;then ( 1 * r1 = 1 or 1 * r2 = 1 ) by A3, A5, XXREAL_0:1;

hence q = (0 * p) + r by A1, A11, RLVECT_1:def 8

.= (0. (TOP-REAL n)) + r by RLVECT_1:10

.= r by RLVECT_1:4 ;

:: thesis: verum