let n be Nat; :: thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg p1,p2 holds
LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2)
let p, p1, p2 be Point of (TOP-REAL n); :: thesis: ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) )

now

assume A1: p in LSeg p1,p2 ; :: thesis: ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) )
then consider r being Real such that
A2: p = ((1 - r) * p1) + (r * p2) and
A3: 0 <= r and
A4: r <= 1 ;

now

per cases ( ( 0 <> r & r <> 1 ) or not 0 <> r or not r <> 1 ) ;

suppose A5: ( 0 <> r & r <> 1 ) ; :: thesis: ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) )

now

let q be set ; :: thesis: ( q in LSeg p1,p2 implies q in (LSeg p1,p) \/ (LSeg p,p2) )
assume q in LSeg p1,p2 ; :: thesis: q in (LSeg p1,p) \/ (LSeg p,p2)
then consider b being Real such that
A6: q = ((1 - b) * p1) + (b * p2) and
A7: 0 <= b and
A8: b <= 1 ;

now

per cases ( b <= r or not b <= r ) ;

suppose A9: b <= r ; :: thesis: q in (LSeg p1,p) \/ (LSeg p,p2)

set x = b * (1 / r);
b * (1 / r) <= r * (1 / r) by A3, A9, XREAL_1:66;
then A10: b * (1 / r) <= 1 by A5, XCMPLX_1:107;
((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * p) = ((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * ((1 - r) * p1)) + ((b * (1 / r)) * (r * p2))) by A2, EUCLID:36
.= (((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * ((1 - r) * p1))) + ((b * (1 / r)) * (r * p2)) by EUCLID:30
.= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + ((b * (1 / r)) * (r * p2)) by EUCLID:34
.= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + (((b * (1 / r)) * r) * p2) by EUCLID:34
.= (((1 - (b * (1 / r))) + ((b * (1 / r)) * (1 - r))) * p1) + (((b * (1 / r)) * r) * p2) by EUCLID:37
.= ((1 - ((b * (1 / r)) * r)) * p1) + (b * p2) by A5, XCMPLX_1:110
.= q by A5, A6, XCMPLX_1:110 ;
then q in { (((1 - lambda) * p1) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A3, A7, A10;
hence q in (LSeg p1,p) \/ (LSeg p,p2) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A11: not b <= r ; :: thesis: q in (LSeg p1,p) \/ (LSeg p,p2)

set bp = 1 - b;
set rp = 1 - r;
set x = (1 - b) * (1 / (1 - r));
A12: 0 <> 1 - r by A5;
r - r = 0 ;
then A13: 0 <= 1 - r by A4, XREAL_1:11;
1 - b <= 1 - r by A11, XREAL_1:12;
then (1 - b) * (1 / (1 - r)) <= (1 - r) * (1 / (1 - r)) by A13, XREAL_1:66;
then A14: (1 - b) * (1 / (1 - r)) <= 1 by A12, XCMPLX_1:107;
A15: 0 <= 1 - b by A8, XREAL_1:50;
A16: 1 - 0 = 1 ;
((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * p) = ((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1))) by A2, EUCLID:36
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2))) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by EUCLID:30
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by EUCLID:34
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by EUCLID:34
.= (((1 - ((1 - b) * (1 / (1 - r)))) + (((1 - b) * (1 / (1 - r))) * (1 - (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by EUCLID:37
.= ((1 - (((1 - b) * (1 / (1 - r))) * (1 - r))) * p2) + ((1 - b) * p1) by A5, A16, XCMPLX_1:110
.= ((1 - (1 - b)) * p2) + ((1 - b) * p1) by A12, XCMPLX_1:110
.= q by A6 ;
then q in { (((1 - lambda) * p2) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A15, A13, A14;
then q in LSeg p,p2 by RLTOPSP1:def 2;
hence q in (LSeg p1,p) \/ (LSeg p,p2) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence q in (LSeg p1,p) \/ (LSeg p,p2) ; :: thesis: verum

end;

then A17: LSeg p1,p2 c= (LSeg p1,p) \/ (LSeg p,p2) by TARSKI:def 3;
A18: LSeg p,p2 c= LSeg p1,p2 by A1, Lm1;
LSeg p1,p c= LSeg p1,p2 by A1, Lm1;
then (LSeg p1,p) \/ (LSeg p,p2) c= LSeg p1,p2 by A18, XBOOLE_1:8;
hence ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) ) by A17, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A19: ( not 0 <> r or not r <> 1 ) ; :: thesis: ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) )

now

per cases ( r = 0 or r = 1 ) by A19;

suppose A20: r = 0 ; :: thesis: LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2)

A21: p in LSeg p,p2 by RLTOPSP1:69;
A22: p = (1 * p1) + (0. (TOP-REAL n)) by A2, A20, EUCLID:33
.= p1 + (0. (TOP-REAL n)) by EUCLID:33
.= p1 by EUCLID:31 ;
then LSeg p1,p = {p} by RLTOPSP1:71;
then LSeg p1,p c= LSeg p,p2 by A21, ZFMISC_1:37;
hence LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) by A22, XBOOLE_1:12; :: thesis: verum

end;

suppose A23: r = 1 ; :: thesis: LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2)

A24: p in LSeg p1,p by RLTOPSP1:69;
A25: p = (0. (TOP-REAL n)) + (1 * p2) by A2, A23, EUCLID:33
.= (0. (TOP-REAL n)) + p2 by EUCLID:33
.= p2 by EUCLID:31 ;
then LSeg p,p2 = {p} by RLTOPSP1:71;
then LSeg p,p2 c= LSeg p1,p by A24, ZFMISC_1:37;
hence LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) by A25, XBOOLE_1:12; :: thesis: verum

end;

end;

end;

hence ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) ) ; :: thesis: verum

end;

end;

end;

hence ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) ) ; :: thesis: verum

end;

hence ( p in LSeg p1,p2 implies LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) ) ; :: thesis: verum