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 = (REAL n) \ { 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 / |.w0.|;
set w2 = (a / |.w0.|) * w1;
set w3 = (a / |.w0.|) * w4;
A4: (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| >= a }

thus (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } c= { q1 where q1 is Point of (TOP-REAL n) : |.q1.| >= a } :: according to XBOOLE_0:def 10 :: thesis:

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: z in (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis:
then reconsider q2 = z as Point of (TOP-REAL n) by EUCLID:22;
not z in { q where q is Point of (TOP-REAL n) : |.q.| < a } by A5, XBOOLE_0:def 5;
then |.q2.| >= a ;
hence z in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| >= a } ; :: thesis:

end;

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| >= a } ; :: thesis:
then consider q1 being Point of (TOP-REAL n) such that
A6: z = q1 and
A7: |.q1.| >= a ;
q1 in the carrier of (TOP-REAL n) ;
then A8: z in REAL n by A6, EUCLID:22;
for q being Point of (TOP-REAL n) st q = z holds
|.q.| >= a by A6, A7;
then not z in { q where q is Point of (TOP-REAL n) : |.q.| < a } ;
hence z in (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } by A8, XBOOLE_0:def 5; :: thesis:

end;

A9: LSeg (w1,((a / |.w0.|) * w1)) c= Q

proof

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

now

per cases ;

case A13: 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) ;
A14: ((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
A16: x = (dist o) . z by FUNCT_1:def 6;
thus x in REAL by A16; :: 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
A17: x in P and
A18: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A17, TOPREAL3:8;
r = dist (w0,o) by A18, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A19: 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 A20: 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 A20, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A19, 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 A21: |.w5.| >= |.w0.| by RLVECT_1:13;
A22: 1 - r >= 0 by A12, XREAL_1:48;
then A23: (abs ((1 - r) + (r * (a / |.w0.|)))) * |.w1.| = ((1 - r) + (r * (a / |.w0.|))) * |.w1.| by A11, A13, ABSVALUE:def 1
.= ((1 - r) * |.w1.|) + ((r * (a / |.w0.|)) * |.w1.|) ;
ex q1 being Point of (TOP-REAL n) st
( q1 = w1 & |.q1.| >= a ) by A1, A4;
then A24: (1 - r) * |.w1.| >= (1 - r) * a by A22, XREAL_1:64;
(r * (a / |.w0.|)) * |.w0.| = ((r * a) / |.w0.|) * |.w0.| by XCMPLX_1:74
.= r * a by A2, XCMPLX_1:87 ;
then (r * (a / |.w0.|)) * |.w1.| >= r * a by A11, A13, A14, A21, XREAL_1:64;
then (abs ((1 - r) + (r * (a / |.w0.|)))) * |.w1.| >= (r * a) + ((1 - r) * a) by A24, A23, XREAL_1:7;
then |.(((1 - r) + (r * (a / |.w0.|))) * w1).| >= a by TOPRNS_1:7;
then |.(((1 - r) * w1) + ((r * (a / |.w0.|)) * w1)).| >= a by EUCLID:33;
hence |.(((1 - r) * w1) + (r * ((a / |.w0.|) * w1))).| >= a by EUCLID:30; :: thesis:

end;

case a <= 0 ; :: thesis:

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

end;

hence x in Q by A1, A4, A10; :: thesis:

end;

A25: LSeg (w4,((a / |.w0.|) * w4)) c= Q

proof

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

now

per cases ;

case A29: 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) ;
A30: ((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
A32: x = (dist o) . z by FUNCT_1:def 6;
thus x in REAL by A32; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
reconsider w59 = w5 as Point of (Euclid n) by TOPREAL3:8;
A33: 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
A34: x in P and
A35: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A34, TOPREAL3:8;
r = dist (w0,o) by A35, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A36: 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 A37: 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 A37, A33, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A36, 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 A38: |.w5.| >= |.w0.| by RLVECT_1:13;
A39: 1 - r >= 0 by A28, XREAL_1:48;
then A40: (abs ((1 - r) + (r * (a / |.w0.|)))) * |.w4.| = ((1 - r) + (r * (a / |.w0.|))) * |.w4.| by A27, A29, ABSVALUE:def 1
.= ((1 - r) * |.w4.|) + ((r * (a / |.w0.|)) * |.w4.|) ;
ex q1 being Point of (TOP-REAL n) st
( q1 = w4 & |.q1.| >= a ) by A1, A4;
then A41: (1 - r) * |.w4.| >= (1 - r) * a by A39, XREAL_1:64;
(r * (a / |.w0.|)) * |.w0.| = ((r * a) / |.w0.|) * |.w0.| by XCMPLX_1:74
.= r * a by A2, XCMPLX_1:87 ;
then (r * (a / |.w0.|)) * |.w4.| >= r * a by A27, A29, A30, A38, XREAL_1:64;
then (abs ((1 - r) + (r * (a / |.w0.|)))) * |.w4.| >= (r * a) + ((1 - r) * a) by A41, A40, XREAL_1:7;
then |.(((1 - r) + (r * (a / |.w0.|))) * w4).| >= a by TOPRNS_1:7;
then |.(((1 - r) * w4) + ((r * (a / |.w0.|)) * w4)).| >= a by EUCLID:33;
hence |.(((1 - r) * w4) + (r * ((a / |.w0.|) * w4))).| >= a by EUCLID:30; :: thesis:

end;

case a <= 0 ; :: thesis:

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

end;

hence x in Q by A1, A4, A26; :: thesis:

end;

A42: LSeg (((a / |.w0.|) * w1),((a / |.w0.|) * w4)) c= Q

proof

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:
A43: abs (a / |.w0.|) = (abs a) / (abs |.w0.|) by COMPLEX1:67
.= (abs a) / |.w0.| by ABSVALUE:def 1 ;
(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
A45: x = (dist o) . z by FUNCT_1:def 6;
thus x in REAL by A45; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
assume x in LSeg (((a / |.w0.|) * w1),((a / |.w0.|) * w4)) ; :: thesis:
then consider r being Real such that
A46: x = ((1 - r) * ((a / |.w0.|) * w1)) + (r * ((a / |.w0.|) * w4)) and
A47: ( 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;
A48: 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
A49: x in P and
A50: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A49, TOPREAL3:8;
r = dist (w0,o) by A50, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A51: 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 A52: w59 in dom (dist o) by FUNCT_2:def 1;
w5 in LSeg (w1,w4) by A47;
then dist (w59,o) in (dist o) .: P by A52, A48, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A51, 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 |.w5.| >= |.w0.| by RLVECT_1:13;
then ( abs a >= 0 & |.w5.| / |.w0.| >= 1 ) by A2, COMPLEX1:46, XREAL_1:181;
then (abs a) * (|.w5.| / |.w0.|) >= (abs a) * 1 by XREAL_1:66;
then (abs a) * (|.w5.| * (|.w0.| ")) >= abs a by XCMPLX_0:def 9;
then ((abs a) * (|.w0.| ")) * |.w5.| >= abs a ;
then A53: ((abs a) / |.w0.|) * |.w5.| >= abs a by XCMPLX_0:def 9;
abs a >= a by ABSVALUE:4;
then ((abs a) / |.w0.|) * |.w5.| >= a by A53, XXREAL_0:2;
then |.((a / |.w0.|) * (((1 - r) * w1) + (r * w4))).| >= a by A43, TOPRNS_1:7;
then |.(((a / |.w0.|) * ((1 - r) * w1)) + ((a / |.w0.|) * (r * w4))).| >= a by EUCLID:32;
then |.(((a / |.w0.|) * ((1 - r) * w1)) + (((a / |.w0.|) * r) * w4)).| >= a by EUCLID:30;
then |.((((a / |.w0.|) * (1 - r)) * w1) + (((a / |.w0.|) * r) * w4)).| >= a by EUCLID:30;
then |.((((1 - r) * (a / |.w0.|)) * w1) + (r * ((a / |.w0.|) * w4))).| >= a by EUCLID:30;
then |.(((1 - r) * ((a / |.w0.|) * w1)) + (r * ((a / |.w0.|) * w4))).| >= a by EUCLID:30;
hence x in Q by A1, A4, A46; :: thesis:

end;

( (a / |.w0.|) * w1 in LSeg (((a / |.w0.|) * w1),((a / |.w0.|) * w4)) & (a / |.w0.|) * w4 in LSeg (((a / |.w0.|) * w1),((a / |.w0.|) * w4)) ) by RLTOPSP1:68;
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 A42, A9, A25; :: thesis: