let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg p1,p2 holds
ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )
let p1, p2 be Point of (TOP-REAL n); :: thesis: for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg p1,p2 holds
ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )
let P be non empty Subset of (TOP-REAL n); :: thesis: ( P is closed & P c= LSeg p1,p2 implies ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) ) )
assume that
A1: P is closed and
A2: P c= LSeg p1,p2 ; :: thesis: ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )
set W = { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } ;
{ r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } or x in REAL )
assume x in { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } ; :: thesis: x in REAL
then ex r being Real st
( r = x & 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) ;
hence x in REAL ; :: thesis: verum

end;

then reconsider W = { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } as Subset of REAL ;
A3: W is bounded_below

proof

take 0 ; :: according to SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in W or 0 <= b₁ )
let r be real number ; :: thesis: ( not r in W or 0 <= r )
assume r in W ; :: thesis: 0 <= r
then ex s being Real st
( s = r & 0 <= s & s <= 1 & ((1 - s) * p1) + (s * p2) in P ) ;
hence 0 <= r ; :: thesis: verum

end;

take r2 = lower_bound W; :: thesis: ( ((1 - r2) * p1) + (r2 * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
r2 <= r ) )

hereby :: thesis: for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
r2 <= r

set p = ((1 - r2) * p1) + (r2 * p2);
assume A4: not ((1 - r2) * p1) + (r2 * p2) in P ; :: thesis: contradiction
then A5: ((1 - r2) * p1) + (r2 * p2) in the carrier of (TOP-REAL n) \ P by XBOOLE_0:def 5;
reconsider u = ((1 - r2) * p1) + (r2 * p2) as Point of (Euclid n) by EUCLID:25;
A6: P ` is open by A1, TOPS_1:29;
X: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider Q = P ` as Subset of (TopSpaceMetr (Euclid n)) ;
Q is open by X, A6, PRE_TOPC:60;
then consider r0 being real number such that
A7: r0 > 0 and
A8: Ball u,r0 c= Q by A5, TOPMETR:22;
A9: ex r0 being Real st r0 in W

proof

consider v being Element of (TOP-REAL n) such that
A10: v in P by SUBSET_1:10;
v in LSeg p1,p2 by A2, A10;
then consider s being Real such that
A11: ( v = ((1 - s) * p1) + (s * p2) & 0 <= s & s <= 1 ) ;
s in { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } by A10, A11;
hence ex r0 being Real st r0 in W ; :: thesis: verum

end;

per cases ( p1 <> p2 or p1 = p2 ) ;

suppose A12: p1 <> p2 ; :: thesis: contradiction

reconsider v1 = p1 as Element of REAL n by EUCLID:25;
reconsider v2 = p2 as Element of REAL n by EUCLID:25;
A13: |.(v2 - v1).| > 0 by A12, EUCLID:20;
then r0 / |.(v2 - v1).| > 0 by A7, XREAL_1:141;
then consider r4 being real number such that
A14: r4 in W and
A15: r4 < r2 + (r0 / |.(v2 - v1).|) by A3, A9, SEQ_4:def 5;
reconsider r4 = r4 as Real by XREAL_0:def 1;
r4 + 0 < r2 + (r0 / |.(v2 - v1).|) by A15;
then A16: r4 - r2 < (r0 / |.(v2 - v1).|) - 0 by XREAL_1:23;
r2 <= r4 by A3, A14, SEQ_4:def 5;
then A17: r4 - r2 >= 0 by XREAL_1:50;
set p3 = ((1 - r4) * p1) + (r4 * p2);
V: p2 - p1 = v2 - v1 by EUCLID:73;
reconsider u3 = ((1 - r4) * p1) + (r4 * p2) as Point of (Euclid n) by EUCLID:25;
U: (((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2)) = (((1 - r4) * p1) + (r4 * p2)) + ((- ((1 - r2) * p1)) - (r2 * p2)) by EUCLID:42
.= ((((1 - r4) * p1) + (r4 * p2)) + (- ((1 - r2) * p1))) + (- (r2 * p2)) by EUCLID:30
.= ((r4 * p2) + (((1 - r4) * p1) + (- ((1 - r2) * p1)))) + (- (r2 * p2)) by EUCLID:30
.= ((((1 - r4) * p1) + (- ((1 - r2) * p1))) + (r4 * p2)) + ((- r2) * p2) by EUCLID:44
.= ((((1 - r4) * p1) + ((- (1 - r2)) * p1)) + (r4 * p2)) + ((- r2) * p2) by EUCLID:44
.= (((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 * p2) + ((- r2) * p2)) by EUCLID:30
.= (((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 + (- r2)) * p2) by EUCLID:37
.= (((1 - r4) + (- (1 - r2))) * p1) + ((r4 - r2) * p2) by EUCLID:37
.= ((- (r4 - r2)) * p1) + ((r4 - r2) * p2)
.= ((r4 - r2) * p2) - ((r4 - r2) * p1) by EUCLID:44
.= (r4 - r2) * (p2 - p1) by EUCLID:53
.= (r4 - r2) * (v2 - v1) by V, EUCLID:69 ;
reconsider v3 = ((1 - r4) * p1) + (r4 * p2), v4 = ((1 - r2) * p1) + (r2 * p2) as Element of REAL n by EUCLID:25;
dist u3,u = |.(v3 - v4).| by Th20
.= |.((((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2))).| by EUCLID:73
.= |.((r4 - r2) * (v2 - v1)).| by U
.= (abs (r4 - r2)) * |.(v2 - v1).| by EUCLID:14
.= (r4 - r2) * |.(v2 - v1).| by A17, ABSVALUE:def 1 ;
then dist u3,u < (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by A13, A16, XREAL_1:70;
then dist u,u3 < r0 by A13, XCMPLX_1:88;
then u3 in { u0 where u0 is Point of (Euclid n) : dist u,u0 < r0 } ;
then A18: u3 in Ball u,r0 by METRIC_1:18;
ex r being Real st
( r = r4 & 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) by A14;
hence contradiction by A8, A18, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A19: p1 = p2 ; :: thesis: contradiction

then A20: ((1 - r2) * p1) + (r2 * p2) = ((1 - r2) + r2) * p1 by EUCLID:37
.= p1 by EUCLID:33 ;
A21: LSeg p1,p2 = {p1} by A19, RLTOPSP1:71;
consider q1 being Point of (TOP-REAL n) such that
A22: q1 in P by SUBSET_1:10;
thus contradiction by A2, A4, A20, A21, A22, TARSKI:def 1; :: thesis: verum

end;

end;

end;

let r be Real; :: thesis: ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P implies r2 <= r )
assume ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) ; :: thesis: r2 <= r
then r in W ;
hence r2 <= r by A3, SEQ_4:def 5; :: thesis: verum