let n be Nat; :: thesis: for a being Real
for Q being Subset of (TOP-REAL n)
for w1, w4 being Point of (TOP-REAL n) st 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 ) ) holds
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 )
let a be Real; :: thesis: for Q being Subset of (TOP-REAL n)
for w1, w4 being Point of (TOP-REAL n) st 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 ) ) holds
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 )
let Q be Subset of (TOP-REAL n); :: thesis: for w1, w4 being Point of (TOP-REAL n) st 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 ) ) holds
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 )
let w1, w4 be Point of (TOP-REAL n); :: thesis: ( 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 ) ) implies 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 ) )
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: 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 )
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 Th28;
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

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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg ((((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4)) or x in Q )
A5: |.((a + 1) / |.w0.|).| = |.(a + 1).| / |.|.w0.|.| by COMPLEX1:67
.= |.(a + 1).| / |.w0.| by ABSVALUE:def 1 ;
(dist o) .: P c= REAL by XREAL_0:def 1;
then reconsider F = (dist o) .: P as Subset of REAL ;
assume x in LSeg ((((a + 1) / |.w0.|) * w1),(((a + 1) / |.w0.|) * w4)) ; :: thesis: x in Q
then consider r being Real such that
A6: x = ((1 - r) * (((a + 1) / |.w0.|) * w1)) + (r * (((a + 1) / |.w0.|) * w4)) and
A7: ( 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;
A8: dist (w59,o) = (dist o) . w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o) .: P

proof

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in (dist o) .: P or 0 <= r )
assume r in (dist o) .: P ; :: thesis: 0 <= r
then consider x being object such that
x in dom (dist o) and
A9: x in P and
A10: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A9, TOPREAL3:8;
r = dist (w0,o) by A10, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis: verum

end;

then A11: F is bounded_below ;
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 A12: w59 in dom (dist o) by FUNCT_2:def 1;
w5 in LSeg (w1,w4) by A7;
then dist (w59,o) in (dist o) .: P by A12, A8, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A11, 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 ( |.(a + 1).| >= 0 & |.w5.| / |.w0.| >= 1 ) by A2, COMPLEX1:46, XREAL_1:181;
then |.(a + 1).| * (|.w5.| / |.w0.|) >= |.(a + 1).| * 1 by XREAL_1:66;
then |.(a + 1).| * ((|.w0.| ") * |.w5.|) >= |.(a + 1).| by XCMPLX_0:def 9;
then (|.(a + 1).| * (|.w0.| ")) * |.w5.| >= |.(a + 1).| ;
then A13: (|.(a + 1).| / |.w0.|) * |.w5.| >= |.(a + 1).| by XCMPLX_0:def 9;
( a + 1 > a & |.(a + 1).| >= a + 1 ) by ABSVALUE:4, XREAL_1:29;
then |.(a + 1).| > a by XXREAL_0:2;
then (|.(a + 1).| / |.w0.|) * |.w5.| > a by A13, XXREAL_0:2;
then |.(((a + 1) / |.w0.|) * (((1 - r) * w1) + (r * w4))).| > a by A5, TOPRNS_1:7;
then |.((((a + 1) / |.w0.|) * ((1 - r) * w1)) + (((a + 1) / |.w0.|) * (r * w4))).| > a by RLVECT_1:def 5;
then |.((((a + 1) / |.w0.|) * ((1 - r) * w1)) + ((((a + 1) / |.w0.|) * r) * w4)).| > a by RLVECT_1:def 7;
then |.(((((a + 1) / |.w0.|) * (1 - r)) * w1) + ((((a + 1) / |.w0.|) * r) * w4)).| > a by RLVECT_1:def 7;
then |.((((1 - r) * ((a + 1) / |.w0.|)) * w1) + (r * (((a + 1) / |.w0.|) * w4))).| > a by RLVECT_1:def 7;
then |.(((1 - r) * (((a + 1) / |.w0.|) * w1)) + (r * (((a + 1) / |.w0.|) * w4))).| > a by RLVECT_1:def 7;
hence x in Q by A1, A6; :: thesis: verum

end;

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

proof

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

now :: thesis: ( ( a >= 0 & |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a ) or ( a < 0 & |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a ) )

per cases ( a >= 0 or a < 0 ) ;

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

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) ;
A21: ((1 - 0) * w4) + (0 * w1) = ((1 - 0) * w4) + (0. (TOP-REAL n)) by RLVECT_1:10
.= (1 - 0) * w4 by RLVECT_1:4
.= w4 by RLVECT_1:def 8 ;
(dist o) .: P c= REAL by XREAL_0:def 1;
then reconsider F = (dist o) .: P as Subset of REAL ;
reconsider w59 = w5 as Point of (Euclid n) by TOPREAL3:8;
A22: dist (w59,o) = (dist o) . w59 by WEIERSTR:def 4;
0 is LowerBound of (dist o) .: P

proof

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in (dist o) .: P or 0 <= r )
assume r in (dist o) .: P ; :: thesis: 0 <= r
then consider x being object such that
x in dom (dist o) and
A23: x in P and
A24: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A23, TOPREAL3:8;
r = dist (w0,o) by A24, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis: verum

end;

then A25: F is bounded_below ;
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 A26: 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 A26, A22, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A25, 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 A27: |.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 A28: (r * ((a + 1) / |.w0.|)) * |.w4.| >= r * (a + 1) by A18, A20, A21, A27, XREAL_1:64;
A29: 1 - r >= 0 by A19, XREAL_1:48;
A30: a + r >= a + 0 by A18, XREAL_1:6;
A31: ex q1 being Point of (TOP-REAL n) st
( q1 = w4 & |.q1.| > a ) by A1;

now :: thesis: ( ( 1 - r > 0 & |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a ) or ( 1 - r <= 0 & |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a ) )

per cases ( 1 - r > 0 or 1 - r <= 0 ) ;

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

then A32: (1 - r) * |.w4.| > (1 - r) * a by A31, XREAL_1:68;
|.((1 - r) + (r * ((a + 1) / |.w0.|))).| * |.w4.| = ((1 - r) + (r * ((a + 1) / |.w0.|))) * |.w4.| by A18, A20, A29, ABSVALUE:def 1
.= ((1 - r) * |.w4.|) + ((r * ((a + 1) / |.w0.|)) * |.w4.|) ;
then |.((1 - r) + (r * ((a + 1) / |.w0.|))).| * |.w4.| > (r * (a + 1)) + ((1 - r) * a) by A28, A32, XREAL_1:8;
then |.((1 - r) + (r * ((a + 1) / |.w0.|))).| * |.w4.| > a by A30, 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 RLVECT_1:def 6;
hence |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a by RLVECT_1:def 7; :: thesis: verum

end;

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

then (1 - r) + r <= 0 + r by XREAL_1:6;
then r = 1 by A19, XXREAL_0:1;
then A33: ((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4)) = (0. (TOP-REAL n)) + (1 * (((a + 1) / |.w0.|) * w4)) by RLVECT_1:10
.= (0. (TOP-REAL n)) + (((a + 1) / |.w0.|) * w4) by RLVECT_1:def 8
.= ((a + 1) / |.w0.|) * w4 by RLVECT_1:4 ;
ex q3 being Point of (TOP-REAL n) st
( q3 = ((a + 1) / |.w0.|) * w4 & |.q3.| > a ) by A1, A15;
hence |.(((1 - r) * w4) + (r * (((a + 1) / |.w0.|) * w4))).| > a by A33; :: thesis: verum

end;

end;

end;

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

end;

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

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

end;

end;

end;

hence x in Q by A1, A17; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (w1,(((a + 1) / |.w0.|) * w1)) or x in Q )
assume x in LSeg (w1,(((a + 1) / |.w0.|) * w1)) ; :: thesis: x in Q
then consider r being Real such that
A36: x = ((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1)) and
A37: 0 <= r and
A38: r <= 1 ;

now :: thesis: ( ( a >= 0 & |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a ) or ( a < 0 & |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a ) )

per cases ( a >= 0 or a < 0 ) ;

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

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) ;
A40: ((1 - 0) * w1) + (0 * w4) = ((1 - 0) * w1) + (0. (TOP-REAL n)) by RLVECT_1:10
.= (1 - 0) * w1 by RLVECT_1:4
.= w1 by RLVECT_1:def 8 ;
(dist o) .: P c= REAL by XREAL_0:def 1;
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 ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in (dist o) .: P or 0 <= r )
assume r in (dist o) .: P ; :: thesis: 0 <= r
then consider x being object such that
x in dom (dist o) and
A41: x in P and
A42: r = (dist o) . x by FUNCT_1:def 6;
reconsider w0 = x as Point of (Euclid n) by A41, TOPREAL3:8;
r = dist (w0,o) by A42, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis: verum

end;

then A43: F is bounded_below ;
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 A44: 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 A44, FUNCT_1:def 6;
then lower_bound F <= dist (w59,o) by A43, 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 A45: |.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 A46: (r * ((a + 1) / |.w0.|)) * |.w1.| >= r * (a + 1) by A37, A39, A40, A45, XREAL_1:64;
A47: ex q1 being Point of (TOP-REAL n) st
( q1 = w1 & |.q1.| > a ) by A1;
A48: a + r >= a + 0 by A37, XREAL_1:6;
A49: 1 - r >= 0 by A38, XREAL_1:48;
A50: ex q2 being Point of (TOP-REAL n) st
( q2 = ((a + 1) / |.w0.|) * w1 & |.q2.| > a ) by A1, A35;

now :: thesis: ( ( 1 - r > 0 & |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a ) or ( 1 - r <= 0 & |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a ) )

per cases ( 1 - r > 0 or 1 - r <= 0 ) ;

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

then A51: (1 - r) * |.w1.| > (1 - r) * a by A47, XREAL_1:68;
|.((1 - r) + (r * ((a + 1) / |.w0.|))).| * |.w1.| = ((1 - r) + (r * ((a + 1) / |.w0.|))) * |.w1.| by A37, A39, A49, ABSVALUE:def 1
.= ((1 - r) * |.w1.|) + ((r * ((a + 1) / |.w0.|)) * |.w1.|) ;
then |.((1 - r) + (r * ((a + 1) / |.w0.|))).| * |.w1.| > (r * (a + 1)) + ((1 - r) * a) by A46, A51, XREAL_1:8;
then |.((1 - r) + (r * ((a + 1) / |.w0.|))).| * |.w1.| > a by A48, 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 RLVECT_1:def 6;
hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a by RLVECT_1:def 7; :: thesis: verum

end;

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

then (1 - r) + r <= 0 + r by XREAL_1:6;
then r = 1 by A38, XXREAL_0:1;
then ((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1)) = (0. (TOP-REAL n)) + (1 * (((a + 1) / |.w0.|) * w1)) by RLVECT_1:10
.= (0. (TOP-REAL n)) + (((a + 1) / |.w0.|) * w1) by RLVECT_1:def 8
.= ((a + 1) / |.w0.|) * w1 by RLVECT_1:4 ;
hence |.(((1 - r) * w1) + (r * (((a + 1) / |.w0.|) * w1))).| > a by A50; :: thesis: verum

end;

end;

end;

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

end;

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

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

end;

end;

end;

hence x in Q by A1, A36; :: thesis: verum

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, A34, A14, A16; :: thesis: verum