let n be Element of NAT ; :: thesis:
let a be Real; :: thesis:
let Q be Subset of (TOP-REAL n); :: thesis:
let w1, w4 be Point of (TOP-REAL n); :: thesis:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P = LSeg (w1,w4) as Subset of (TopSpaceMetr (Euclid n)) ;
assume A1: ( Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } & w1 in Q & w4 in Q & ( for r being Real holds
( not w1 = r * w4 & not w4 = r * w1 ) ) ) ; :: thesis:
then not 0. (TOP-REAL n) in LSeg (w1,w4) by RLTOPSP1:71;
then consider w0 being Point of (TOP-REAL n) such that
w0 in LSeg (w1,w4) and
A2: |.w0.| > 0 and
A3: |.w0.| = (dist_min P) . (0. (TOP-REAL n)) by Th48;
set l9 = (a + 1) / |.w0.|;
set w2 = ((a + 1) / |.w0.|) * w1;
set w3 = ((a + 1) / |.w0.|) * w4;
A4: LSeg ((((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4)) c= Q

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P = LSeg (w1,w4) as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
let x be set ; :: according to TARSKI:def 3 :: thesis:
A5: abs ((a + 1) / |.w0.|) = (abs (a + 1)) / (abs |.w0.|) by COMPLEX1:67
.= (abs (a + 1)) / |.w0.| by ABSVALUE:def 1 ;
(dist o) .: P c= REAL

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (dist o) .: P ; :: thesis:
then consider z being set such that
z in dom (dist o) and
z in P and
A7: x = (dist o) . z by FUNCT_1:def 6;
thus x in REAL by A7; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
assume x in LSeg ((((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4)) ; :: thesis:
then consider r being Real such that
A8: x = ((1 - r) * (((a + 1) / |.w0.|) * w1)) + (r * (((a + 1) / |.w0.|) * w4)) and
A9: ( 0 <= r & r <= 1 ) ;
reconsider w5 = ((1 - r) * w1) + (r * w4) as Point of (TOP-REAL n) ;
reconsider w59 = w5 as Point of (Euclid n) by TOPREAL3:8;
A10: dist (w59,o) = (dist o) . w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o) .: P

proof

let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis:
assume r in (dist o) .: P ; :: thesis:
then consider x being set such that
x in dom (dist o) and
A11: x in P and
A12: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A11, TOPREAL3:8;
r = dist (w0,o) by A12, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

end;

A16: ((a + 1) / |.w0.|) * w4 in LSeg ((((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4)) by RLTOPSP1:68;
then A17: ((a + 1) / |.w0.|) * w4 in Q by A4;
A18: LSeg (w4,(((a + 1) / |.w0.|) * w4)) c= Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in LSeg (w4,(((a + 1) / |.w0.|) * w4)) ; :: thesis:
then consider r being Real such that
A19: x = ((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4)) and
A20: 0 <= r and
A21: r <= 1 ;

now

per cases ;

case A22: a >= 0 ; :: thesis:

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P = LSeg (w4,w1) as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
reconsider w5 = ((1 - 0) * w4) + (0 * w1) as Point of (TOP-REAL n) ;
A23: ((1 - 0) * w4) + (0 * w1) = ((1 - 0) * w4) + (0. (TOP-REAL n)) by EUCLID:29
.= (1 - 0) * w4 by EUCLID:27
.= w4 by EUCLID:29 ;
(dist o) .: P c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (dist o) .: P ; :: thesis:
then consider z being set such that
z in dom (dist o) and
z in P and
A25: x = (dist o) . z by FUNCT_1:def 6;
thus x in REAL by A25; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
reconsider w59 = w5 as Point of (Euclid n) by TOPREAL3:8;
A26: dist (w59,o) = (dist o) . w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o) .: P

proof

let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis:
assume r in (dist o) .: P ; :: thesis:
then consider x being set such that
x in dom (dist o) and
A27: x in P and
A28: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A27, TOPREAL3:8;
r = dist (w0,o) by A28, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A29: F is bounded_below by XXREAL_2:def 9;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then w59 in the carrier of (TopSpaceMetr (Euclid n)) ;
then A30: w59 in dom (dist o) by FUNCT_2:def 1;
w5 in { (((1 - r1) * w4) + (r1 * w1)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } ;
then dist (w59,o) in (dist o) .: P by A30, A26, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A29, SEQ_4:def 2;
then dist (w59,o) >= lower_bound ([#] ((dist o) .: P)) by WEIERSTR:def 1;
then dist (w59,o) >= lower_bound ((dist o) .: P) by WEIERSTR:def 3;
then dist (w59,o) >= |.w0.| by A3, WEIERSTR:def 6;
then |.(w5 - (0. (TOP-REAL n))).| >= |.w0.| by JGRAPH_1:28;
then A31: |.w5.| >= |.w0.| by RLVECT_1:13;
(r * ((a + 1) / |.w0.|)) * |.w0.| = ((r * (a + 1)) / |.w0.|) * |.w0.| by XCMPLX_1:74
.= r * (a + 1) by A2, XCMPLX_1:87 ;
then A32: (r * ((a + 1) / |.w0.|)) * |.w4.| >= r * (a + 1) by A20, A22, A23, A31, XREAL_1:64;
A33: 1 - r >= 0 by A21, XREAL_1:48;
A34: a + r >= a + 0 by A20, XREAL_1:6;
A35: ex q1 being Point of (TOP-REAL n) st
( q1 = w4 & |.q1.| > a ) by A1;

now

per cases ;

case 1 - r > 0 ; :: thesis:

then A36: (1 - r) * |.w4.| > (1 - r) * a by A35, XREAL_1:68;
(abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w4.| = ((1 - r) + (r * ((a + 1) / |.w0.|))) * |.w4.| by A20, A22, A33, ABSVALUE:def 1
.= ((1 - r) * |.w4.|) + ((r * ((a + 1) / |.w0.|)) * |.w4.|) ;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w4.| > (r * (a + 1)) + ((1 - r) * a) by A32, A36, XREAL_1:8;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w4.| > a by A34, XXREAL_0:2;
then |.(((1 - r) + (r * ((a + 1) / |.w0.|))) * w4).| > a by TOPRNS_1:7;
then |.(((1 - r) * w4) + ((r * ((a + 1) / |.w0.|)) * w4)).| > a by EUCLID:33;
hence |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a by EUCLID:30; :: thesis:

end;

case 1 - r <= 0 ; :: thesis:

then (1 - r) + r <= 0 + r by XREAL_1:6;
then r = 1 by A21, XXREAL_0:1;
then A37: ((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4)) = (0. (TOP-REAL n)) + (1 * (((a + 1) / |.w0.|) * w4)) by EUCLID:29
.= (0. (TOP-REAL n)) + (((a + 1) / |.w0.|) * w4) by EUCLID:29
.= ((a + 1) / |.w0.|) * w4 by EUCLID:27 ;
ex q3 being Point of (TOP-REAL n) st
( q3 = ((a + 1) / |.w0.|) * w4 & |.q3.| > a ) by A1, A17;
hence |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a by A37; :: thesis:

end;

hence |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a ; :: thesis:

end;

case a < 0 ; :: thesis:

hence |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a ; :: thesis:

end;

hence x in Q by A1, A19; :: thesis:

end;

A38: ((a + 1) / |.w0.|) * w1 in LSeg ((((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4)) by RLTOPSP1:68;
then A39: ((a + 1) / |.w0.|) * w1 in Q by A4;
LSeg (w1,(((a + 1) / |.w0.|) * w1)) c= Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in LSeg (w1,(((a + 1) / |.w0.|) * w1)) ; :: thesis:
then consider r being Real such that
A40: x = ((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1)) and
A41: 0 <= r and
A42: r <= 1 ;

now

per cases ;

case A43: a >= 0 ; :: thesis:

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P = LSeg (w1,w4) as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
reconsider w5 = ((1 - 0) * w1) + (0 * w4) as Point of (TOP-REAL n) ;
A44: ((1 - 0) * w1) + (0 * w4) = ((1 - 0) * w1) + (0. (TOP-REAL n)) by EUCLID:29
.= (1 - 0) * w1 by EUCLID:27
.= w1 by EUCLID:29 ;
(dist o) .: P c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (dist o) .: P ; :: thesis:
then consider z being set such that
z in dom (dist o) and
z in P and
A46: x = (dist o) . z by FUNCT_1:def 6;
thus x in REAL by A46; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
reconsider w59 = w5 as Point of (Euclid n) by TOPREAL3:8;
0 is LowerBound of (dist o) .: P

proof

let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis:
assume r in (dist o) .: P ; :: thesis:
then consider x being set such that
x in dom (dist o) and
A47: x in P and
A48: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A47, TOPREAL3:8;
r = dist (w0,o) by A48, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A49: F is bounded_below by XXREAL_2:def 9;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then w59 in the carrier of (TopSpaceMetr (Euclid n)) ;
then A50: w59 in dom (dist o) by FUNCT_2:def 1;
( w5 in LSeg (w1,w4) & dist (w59,o) = (dist o) . w59 ) by WEIERSTR:def 4;
then dist (w59,o) in (dist o) .: P by A50, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A49, SEQ_4:def 2;
then dist (w59,o) >= lower_bound ([#] ((dist o) .: P)) by WEIERSTR:def 1;
then dist (w59,o) >= lower_bound ((dist o) .: P) by WEIERSTR:def 3;
then dist (w59,o) >= |.w0.| by A3, WEIERSTR:def 6;
then |.(w5 - (0. (TOP-REAL n))).| >= |.w0.| by JGRAPH_1:28;
then A51: |.w5.| >= |.w0.| by RLVECT_1:13;
(r * ((a + 1) / |.w0.|)) * |.w0.| = ((r * (a + 1)) / |.w0.|) * |.w0.| by XCMPLX_1:74
.= r * (a + 1) by A2, XCMPLX_1:87 ;
then A52: (r * ((a + 1) / |.w0.|)) * |.w1.| >= r * (a + 1) by A41, A43, A44, A51, XREAL_1:64;
A53: ex q1 being Point of (TOP-REAL n) st
( q1 = w1 & |.q1.| > a ) by A1;
A54: a + r >= a + 0 by A41, XREAL_1:6;
A55: 1 - r >= 0 by A42, XREAL_1:48;
A56: ex q2 being Point of (TOP-REAL n) st
( q2 = ((a + 1) / |.w0.|) * w1 & |.q2.| > a ) by A1, A39;

now

per cases ;

case 1 - r > 0 ; :: thesis:

then A57: (1 - r) * |.w1.| > (1 - r) * a by A53, XREAL_1:68;
(abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w1.| = ((1 - r) + (r * ((a + 1) / |.w0.|))) * |.w1.| by A41, A43, A55, ABSVALUE:def 1
.= ((1 - r) * |.w1.|) + ((r * ((a + 1) / |.w0.|)) * |.w1.|) ;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w1.| > (r * (a + 1)) + ((1 - r) * a) by A52, A57, XREAL_1:8;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w1.| > a by A54, XXREAL_0:2;
then |.(((1 - r) + (r * ((a + 1) / |.w0.|))) * w1).| > a by TOPRNS_1:7;
then |.(((1 - r) * w1) + ((r * ((a + 1) / |.w0.|)) * w1)).| > a by EUCLID:33;
hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a by EUCLID:30; :: thesis:

end;

case 1 - r <= 0 ; :: thesis:

then (1 - r) + r <= 0 + r by XREAL_1:6;
then r = 1 by A42, XXREAL_0:1;
then ((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1)) = (0. (TOP-REAL n)) + (1 * (((a + 1) / |.w0.|) * w1)) by EUCLID:29
.= (0. (TOP-REAL n)) + (((a + 1) / |.w0.|) * w1) by EUCLID:29
.= ((a + 1) / |.w0.|) * w1 by EUCLID:27 ;
hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a by A56; :: thesis:

end;

hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a ; :: thesis:

end;

case a < 0 ; :: thesis:

hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a ; :: thesis:

end;

hence x in Q by A1, A40; :: thesis:

end;

hence ex w2, w3 being Point of (TOP-REAL n) st
( w2 in Q & w3 in Q & LSeg (w1,w2) c= Q & LSeg (w2,w3) c= Q & LSeg (w3,w4) c= Q ) by A4, A38, A16, A18; :: thesis: