let n be 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 ) ) )
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 object ; :: 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 by XREAL_0:def 1; :: 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 ;
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 ) )
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 ) )
A3: W is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of W
let r be ExtReal; :: according to XXREAL_2:def 2 :: 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;

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);
reconsider u = ((1 - r2) * p1) + (r2 * p2) as Point of (Euclid n) by EUCLID:22;
A4: 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)) ;
P ` is open by A1, TOPS_1:3;
then A5: Q is open by A4, PRE_TOPC:30;
A6: ex r0 being Real st r0 in W

proof

consider v being Element of (TOP-REAL n) such that
A7: v in P by SUBSET_1:4;
v in LSeg (p1,p2) by A2, A7;
then consider s being Real such that
A8: ( 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 A7, A8;
hence ex r0 being Real st r0 in W ; :: thesis: verum

end;

assume A9: not ((1 - r2) * p1) + (r2 * p2) in P ; :: thesis: contradiction
then ((1 - r2) * p1) + (r2 * p2) in the carrier of (TOP-REAL n) \ P by XBOOLE_0:def 5;
then consider r0 being Real such that
A10: r0 > 0 and
A11: Ball (u,r0) c= Q by A5, TOPMETR:15;

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

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

reconsider v2 = p2 as Element of REAL n by EUCLID:22;
reconsider v1 = p1 as Element of REAL n by EUCLID:22;
A13: |.(v2 - v1).| > 0 by A12, EUCLID:17;
then r0 / |.(v2 - v1).| > 0 by A10, XREAL_1:139;
then consider r4 being Real such that
A14: r4 in W and
A15: r4 < r2 + (r0 / |.(v2 - v1).|) by A3, A6, SEQ_4:def 2;
reconsider r4 = r4 as Real ;
r4 + 0 < r2 + (r0 / |.(v2 - v1).|) by A15;
then A16: r4 - r2 < (r0 / |.(v2 - v1).|) - 0 by XREAL_1:21;
set p3 = ((1 - r4) * p1) + (r4 * p2);
reconsider u3 = ((1 - r4) * p1) + (r4 * p2) as Point of (Euclid n) by EUCLID:22;
reconsider v3 = ((1 - r4) * p1) + (r4 * p2), v4 = ((1 - r2) * p1) + (r2 * p2) as Element of REAL n by EUCLID:22;
A17: (((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2)) = (((1 - r4) * p1) + (r4 * p2)) + ((- ((1 - r2) * p1)) - (r2 * p2)) by RLVECT_1:30
.= ((((1 - r4) * p1) + (r4 * p2)) + (- ((1 - r2) * p1))) + (- (r2 * p2)) by RLVECT_1:def 3
.= ((r4 * p2) + (((1 - r4) * p1) + (- ((1 - r2) * p1)))) + (- (r2 * p2)) by RLVECT_1:def 3
.= ((((1 - r4) * p1) + (- ((1 - r2) * p1))) + (r4 * p2)) + ((- r2) * p2) by RLVECT_1:79
.= ((((1 - r4) * p1) + ((- (1 - r2)) * p1)) + (r4 * p2)) + ((- r2) * p2) by RLVECT_1:79
.= (((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 * p2) + ((- r2) * p2)) by RLVECT_1:def 3
.= (((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 + (- r2)) * p2) by RLVECT_1:def 6
.= (((1 - r4) + (- (1 - r2))) * p1) + ((r4 - r2) * p2) by RLVECT_1:def 6
.= ((- (r4 - r2)) * p1) + ((r4 - r2) * p2)
.= ((r4 - r2) * p2) - ((r4 - r2) * p1) by RLVECT_1:79
.= (r4 - r2) * (p2 - p1) by RLVECT_1:34
.= (r4 - r2) * (v2 - v1) ;
r2 <= r4 by A3, A14, SEQ_4:def 2;
then A18: r4 - r2 >= 0 by XREAL_1:48;
dist (u3,u) = |.(v3 - v4).| by Th5
.= |.((((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2))).|
.= |.((r4 - r2) * (v2 - v1)).| by A17
.= |.(r4 - r2).| * |.(v2 - v1).| by EUCLID:11
.= (r4 - r2) * |.(v2 - v1).| by A18, ABSVALUE:def 1 ;
then dist (u3,u) < (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by A13, A16, XREAL_1:68;
then dist (u,u3) < r0 by A13, XCMPLX_1:87;
then u3 in { u0 where u0 is Point of (Euclid n) : dist (u,u0) < r0 } ;
then A19: u3 in Ball (u,r0) by METRIC_1:17;
ex r being Real st
( r = r4 & 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) by A14;
hence contradiction by A11, A19, XBOOLE_0:def 5; :: thesis: verum

end;

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

then A21: LSeg (p1,p2) = {p1} by RLTOPSP1:70;
A22: ex q1 being Point of (TOP-REAL n) st q1 in P by SUBSET_1:4;
((1 - r2) * p1) + (r2 * p2) = ((1 - r2) + r2) * p1 by A20, RLVECT_1:def 6
.= p1 by RLVECT_1:def 8 ;
hence contradiction by A2, A9, 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 2; :: thesis: verum