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:
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 A2: not 0. (TOP-REAL n) in LSeg w1,w4 by RLTOPSP1:72;
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then reconsider P = LSeg w1,w4 as Subset of (TopSpaceMetr (Euclid n)) by XX, YY, V;
consider w0 being Point of (TOP-REAL n) such that
A3: ( w0 in LSeg w1,w4 & |.w0.| > 0 & |.w0.| = (dist_min P) . (0. (TOP-REAL n)) ) by A2, Th48;
set l' = (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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in LSeg (((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4) ; :: thesis:
then x in { (((1 - r) * (((a + 1) / |.w0.|) * w1)) + (r * (((a + 1) / |.w0.|) * w4))) where r is Real : ( 0 <= r & r <= 1 ) } ;
then consider r being Real such that
A5: ( x = ((1 - r) * (((a + 1) / |.w0.|) * w1)) + (r * (((a + 1) / |.w0.|) * w4)) & 0 <= r & r <= 1 ) ;
reconsider w5 = ((1 - r) * w1) + (r * w4) as Point of (TOP-REAL n) ;
reconsider w5' = w5 as Point of (Euclid n) by TOPREAL3:13;
w5 in { (((1 - r1) * w1) + (r1 * w4)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A5;
then A6: w5 in LSeg w1,w4 ;
U: the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by XX, YY;
V: 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)) by XX, YY, U;
(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
A7: ( z in dom (dist o) & z in P & x = (dist o) . z ) by FUNCT_1:def 12;
reconsider z2 = z as Point of (Euclid n) by A7, TOPREAL3:13;
(dist o) . z2 = dist z2,o by WEIERSTR:def 6;
hence x in REAL by A7; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then A8: w5' in the carrier of (TopSpaceMetr (Euclid n)) by XX, YY;
for r being real number st r in (dist o) .: P holds
0 <= r

proof

let r be real number ; :: thesis:
assume r in (dist o) .: P ; :: thesis:
then consider x being set such that
A9: ( x in dom (dist o) & x in P & r = (dist o) . x ) by FUNCT_1:def 12;
reconsider w0 = x as Point of (Euclid n) by A9, TOPREAL3:13;
r = dist w0,o by A9, WEIERSTR:def 6;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A10: F is bounded_below by SEQ_4:def 2;
( w5' in dom (dist o) & dist w5',o = (dist o) . w5' ) by A8, FUNCT_2:def 1, WEIERSTR:def 6;
then dist w5',o in (dist o) .: P by A6, FUNCT_1:def 12;
then lower_bound F <= dist w5',o by A10, SEQ_4:def 5;
then dist w5',o >= lower_bound ([#] ((dist o) .: P)) by WEIERSTR:def 3;
then dist w5',o >= lower_bound ((dist o) .: P) by WEIERSTR:def 5;
then dist w5',o >= |.w0.| by A3, WEIERSTR:def 8;
then |.(w5 - (0. (TOP-REAL n))).| >= |.w0.| by JGRAPH_1:45;
then A11: |.w5.| >= |.w0.| by RLVECT_1:26, RLVECT_1:27;
A12: abs (a + 1) >= 0 by COMPLEX1:132;
A13: abs ((a + 1) / |.w0.|) = (abs (a + 1)) / (abs |.w0.|) by COMPLEX1:153
.= (abs (a + 1)) / |.w0.| by ABSVALUE:def 1 ;
|.w5.| / |.w0.| >= 1 by A3, A11, XREAL_1:183;
then (abs (a + 1)) * (|.w5.| / |.w0.|) >= (abs (a + 1)) * 1 by A12, XREAL_1:68;
then (abs (a + 1)) * ((|.w0.| " ) * |.w5.|) >= abs (a + 1) by XCMPLX_0:def 9;
then ((abs (a + 1)) * (|.w0.| " )) * |.w5.| >= abs (a + 1) ;
then A14: ((abs (a + 1)) / |.w0.|) * |.w5.| >= abs (a + 1) by XCMPLX_0:def 9;
A15: a + 1 > a by XREAL_1:31;
abs (a + 1) >= a + 1 by ABSVALUE:11;
then abs (a + 1) > a by A15, XXREAL_0:2;
then ((abs (a + 1)) / |.w0.|) * |.w5.| > a by A14, XXREAL_0:2;
then |.(((a + 1) / |.w0.|) * (((1 - r) * w1) + (r * w4))).| > a by A13, TOPRNS_1:8;
then |.((((a + 1) / |.w0.|) * ((1 - r) * w1)) + (((a + 1) / |.w0.|) * (r * w4))).| > a by EUCLID:36;
then |.((((a + 1) / |.w0.|) * ((1 - r) * w1)) + ((((a + 1) / |.w0.|) * r) * w4)).| > a by EUCLID:34;
then |.(((((a + 1) / |.w0.|) * (1 - r)) * w1) + ((((a + 1) / |.w0.|) * r) * w4)).| > a by EUCLID:34;
then |.((((1 - r) * ((a + 1) / |.w0.|)) * w1) + (r * (((a + 1) / |.w0.|) * w4))).| > a by EUCLID:34;
then |.(((1 - r) * (((a + 1) / |.w0.|) * w1)) + (r * (((a + 1) / |.w0.|) * w4))).| > a by EUCLID:34;
hence x in Q by A1, A5; :: thesis:

end;

A16: ( ((a + 1) / |.w0.|) * w1 in LSeg (((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4) & ((a + 1) / |.w0.|) * w4 in LSeg (((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4) ) by RLTOPSP1:69;
then A17: ((a + 1) / |.w0.|) * w1 in Q by A4;
A18: ((a + 1) / |.w0.|) * w4 in Q by A4, A16;
A19: 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 x in { (((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))) where r is Real : ( 0 <= r & r <= 1 ) } ;
then consider r being Real such that
A20: ( x = ((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1)) & 0 <= r & r <= 1 ) ;

now

per cases ;

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

(a + 1) / |.w0.| > 0 by A3, A21, XREAL_1:141;
then A22: r * ((a + 1) / |.w0.|) >= 0 by A20;
reconsider w5 = ((1 - 0 ) * w1) + (0 * w4) as Point of (TOP-REAL n) ;
A23: ((1 - 0 ) * w1) + (0 * w4) = ((1 - 0 ) * w1) + (0. (TOP-REAL n)) by EUCLID:33
.= (1 - 0 ) * w1 by EUCLID:31
.= w1 by EUCLID:33 ;
reconsider w5' = w5 as Point of (Euclid n) by TOPREAL3:13;
w5 in { (((1 - r1) * w1) + (r1 * w4)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } ;
then A24: w5 in LSeg w1,w4 ;
U: the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by XX, YY;
V: 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)) by U;
(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
A25: ( z in dom (dist o) & z in P & x = (dist o) . z ) by FUNCT_1:def 12;
reconsider z2 = z as Point of (Euclid n) by A25, TOPREAL3:13;
(dist o) . z2 = dist z2,o by WEIERSTR:def 6;
hence x in REAL by A25; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then A26: w5' in the carrier of (TopSpaceMetr (Euclid n)) by XX, YY, V;
for r being real number st r in (dist o) .: P holds
0 <= r

proof

let r be real number ; :: thesis:
assume r in (dist o) .: P ; :: thesis:
then consider x being set such that
A27: ( x in dom (dist o) & x in P & r = (dist o) . x ) by FUNCT_1:def 12;
reconsider w0 = x as Point of (Euclid n) by A27, TOPREAL3:13;
r = dist w0,o by A27, WEIERSTR:def 6;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A28: F is bounded_below by SEQ_4:def 2;
( w5' in dom (dist o) & dist w5',o = (dist o) . w5' ) by A26, FUNCT_2:def 1, WEIERSTR:def 6;
then dist w5',o in (dist o) .: P by A24, FUNCT_1:def 12;
then lower_bound F <= dist w5',o by A28, SEQ_4:def 5;
then dist w5',o >= lower_bound ([#] ((dist o) .: P)) by WEIERSTR:def 3;
then dist w5',o >= lower_bound ((dist o) .: P) by WEIERSTR:def 5;
then dist w5',o >= |.w0.| by A3, WEIERSTR:def 8;
then |.(w5 - (0. (TOP-REAL n))).| >= |.w0.| by JGRAPH_1:45;
then A29: |.w5.| >= |.w0.| by RLVECT_1:26, RLVECT_1:27;
(r * ((a + 1) / |.w0.|)) * |.w0.| = ((r * (a + 1)) / |.w0.|) * |.w0.| by XCMPLX_1:75
.= r * (a + 1) by A3, XCMPLX_1:88 ;
then A30: (r * ((a + 1) / |.w0.|)) * |.w1.| >= r * (a + 1) by A22, A23, A29, XREAL_1:66;
consider q1 being Point of (TOP-REAL n) such that
A31: ( q1 = w1 & |.q1.| > a ) by A1;
consider q2 being Point of (TOP-REAL n) such that
A32: ( q2 = ((a + 1) / |.w0.|) * w1 & |.q2.| > a ) by A1, A17;
A33: 1 - r >= 0 by A20, XREAL_1:50;
A34: a + r >= a + 0 by A20, XREAL_1:8;

now

per cases ;

case 1 - r > 0 ; :: thesis:

then A35: (1 - r) * |.w1.| > (1 - r) * a by A31, XREAL_1:70;
(1 - r) + (r * ((a + 1) / |.w0.|)) >= 0 by A22, A33;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w1.| = ((1 - r) + (r * ((a + 1) / |.w0.|))) * |.w1.| by 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 A30, A35, XREAL_1:10;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w1.| > a by A34, XXREAL_0:2;
then |.(((1 - r) + (r * ((a + 1) / |.w0.|))) * w1).| > a by TOPRNS_1:8;
then |.(((1 - r) * w1) + ((r * ((a + 1) / |.w0.|)) * w1)).| > a by EUCLID:37;
hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a by EUCLID:34; :: thesis:

end;

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

then (1 - r) + r <= 0 + r by XREAL_1:8;
then r = 1 by A20, XXREAL_0:1;
then ((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1)) = (0. (TOP-REAL n)) + (1 * (((a + 1) / |.w0.|) * w1)) by EUCLID:33
.= (0. (TOP-REAL n)) + (((a + 1) / |.w0.|) * w1) by EUCLID:33
.= ((a + 1) / |.w0.|) * w1 by EUCLID:31 ;
hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a by A32; :: 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, A20; :: thesis:

end;

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 x in { (((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))) where r is Real : ( 0 <= r & r <= 1 ) } ;
then consider r being Real such that
A36: ( x = ((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4)) & 0 <= r & r <= 1 ) ;

now

per cases ;

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

(a + 1) / |.w0.| > 0 by A3, A37, XREAL_1:141;
then A38: r * ((a + 1) / |.w0.|) >= 0 by A36;
reconsider w5 = ((1 - 0 ) * w4) + (0 * w1) as Point of (TOP-REAL n) ;
A39: ((1 - 0 ) * w4) + (0 * w1) = ((1 - 0 ) * w4) + (0. (TOP-REAL n)) by EUCLID:33
.= (1 - 0 ) * w4 by EUCLID:31
.= w4 by EUCLID:33 ;
reconsider w5' = w5 as Point of (Euclid n) by TOPREAL3:13;
w5 in { (((1 - r1) * w4) + (r1 * w1)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } ;
then A40: w5 in LSeg w1,w4 by RLTOPSP1:def 2;
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
U: the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by XX, YY;
reconsider P = LSeg w4,w1 as Subset of (TopSpaceMetr (Euclid n)) by XX, YY, U, V;
(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
A41: ( z in dom (dist o) & z in P & x = (dist o) . z ) by FUNCT_1:def 12;
reconsider z2 = z as Point of (Euclid n) by A41, TOPREAL3:13;
(dist o) . z2 = dist z2,o by WEIERSTR:def 6;
hence x in REAL by A41; :: thesis:

end;

then reconsider F = (dist o) .: P as Subset of REAL ;
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then A42: w5' in the carrier of (TopSpaceMetr (Euclid n)) by XX, YY, V;
for r being real number st r in (dist o) .: P holds
0 <= r

proof

let r be real number ; :: thesis:
assume r in (dist o) .: P ; :: thesis:
then consider x being set such that
A43: ( x in dom (dist o) & x in P & r = (dist o) . x ) by FUNCT_1:def 12;
reconsider w0 = x as Point of (Euclid n) by A43, TOPREAL3:13;
r = dist w0,o by A43, WEIERSTR:def 6;
hence 0 <= r by METRIC_1:5; :: thesis:

end;

then A44: F is bounded_below by SEQ_4:def 2;
( w5' in dom (dist o) & dist w5',o = (dist o) . w5' ) by A42, FUNCT_2:def 1, WEIERSTR:def 6;
then dist w5',o in (dist o) .: P by A40, FUNCT_1:def 12;
then lower_bound F <= dist w5',o by A44, SEQ_4:def 5;
then dist w5',o >= lower_bound ([#] ((dist o) .: P)) by WEIERSTR:def 3;
then dist w5',o >= lower_bound ((dist o) .: P) by WEIERSTR:def 5;
then dist w5',o >= |.w0.| by A3, WEIERSTR:def 8;
then |.(w5 - (0. (TOP-REAL n))).| >= |.w0.| by JGRAPH_1:45;
then A45: |.w5.| >= |.w0.| by RLVECT_1:26, RLVECT_1:27;
(r * ((a + 1) / |.w0.|)) * |.w0.| = ((r * (a + 1)) / |.w0.|) * |.w0.| by XCMPLX_1:75
.= r * (a + 1) by A3, XCMPLX_1:88 ;
then A46: (r * ((a + 1) / |.w0.|)) * |.w4.| >= r * (a + 1) by A38, A39, A45, XREAL_1:66;
consider q1 being Point of (TOP-REAL n) such that
A47: ( q1 = w4 & |.q1.| > a ) by A1;
A48: 1 - r >= 0 by A36, XREAL_1:50;
A49: a + r >= a + 0 by A36, XREAL_1:8;

now

per cases ;

case 1 - r > 0 ; :: thesis:

then A50: (1 - r) * |.w4.| > (1 - r) * a by A47, XREAL_1:70;
(1 - r) + (r * ((a + 1) / |.w0.|)) >= 0 by A38, A48;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w4.| = ((1 - r) + (r * ((a + 1) / |.w0.|))) * |.w4.| by 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 A46, A50, XREAL_1:10;
then (abs ((1 - r) + (r * ((a + 1) / |.w0.|)))) * |.w4.| > a by A49, XXREAL_0:2;
then |.(((1 - r) + (r * ((a + 1) / |.w0.|))) * w4).| > a by TOPRNS_1:8;
then |.(((1 - r) * w4) + ((r * ((a + 1) / |.w0.|)) * w4)).| > a by EUCLID:37;
hence |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a by EUCLID:34; :: thesis:

end;

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

then (1 - r) + r <= 0 + r by XREAL_1:8;
then r = 1 by A36, XXREAL_0:1;
then A51: ((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4)) = (0. (TOP-REAL n)) + (1 * (((a + 1) / |.w0.|) * w4)) by EUCLID:33
.= (0. (TOP-REAL n)) + (((a + 1) / |.w0.|) * w4) by EUCLID:33
.= ((a + 1) / |.w0.|) * w4 by EUCLID:31 ;
consider q3 being Point of (TOP-REAL n) such that
A52: ( q3 = ((a + 1) / |.w0.|) * w4 & |.q3.| > a ) by A1, A18;
thus |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a by A51, A52; :: 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, A36; :: 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, A16, A19; :: thesis: