:: WEIERSTR semantic presentation

begin

theorem Th1: :: WEIERSTR:1
for M being MetrSpace
for x1, x2 being Point of M
for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
proof
let M be MetrSpace; ::_thesis: for x1, x2 being Point of M
for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
let x1, x2 be Point of M; ::_thesis: for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
let r1, r2 be Real; ::_thesis: ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
reconsider x = x1 as Point of M ;
reconsider r = ((abs r1) + (abs r2)) + (dist (x1,x2)) as Real ;
take  x ; ::_thesis: ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
take  r ; ::_thesis: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
 for a being set st a in (Ball (x1,r1)) \/ (Ball (x2,r2)) holds
a in Ball (x,r)
proof
let a be set ; ::_thesis: ( a in (Ball (x1,r1)) \/ (Ball (x2,r2)) implies a in Ball (x,r) )
assume A1: a in (Ball (x1,r1)) \/ (Ball (x2,r2)) ; ::_thesis: a in Ball (x,r)
then reconsider a = a as Point of M ;
now__::_thesis:_(_(_a_in_Ball_(x1,r1)_&_a_in_Ball_(x,r)_)_or_(_a_in_Ball_(x2,r2)_&_a_in_Ball_(x,r)_)_)
percases ( a in Ball (x1,r1) or a in Ball (x2,r2) ) by A1, XBOOLE_0:def_3;
caseA2: a in Ball (x1,r1) ; ::_thesis: a in Ball (x,r)
 ( r1 <= abs r1 & 0 <= abs r2 ) by ABSVALUE:4, COMPLEX1:46;
then A3: r1 + 0 <= (abs r1) + (abs r2) by XREAL_1:7;
A4: dist (x,a) < r1 by A2, METRIC_1:11;
 0 <= dist (x1,x2) by METRIC_1:5;
then  r1 + 0 <= ((abs r1) + (abs r2)) + (dist (x1,x2)) by A3, XREAL_1:7;
then  (dist (x,a)) - r < r1 - r1 by A4, XREAL_1:14;
then A5: ((dist (x,a)) - r) + r < 0 + r by XREAL_1:8;
 not M is empty by A2;
hence  a in Ball (x,r) by A5, METRIC_1:11; ::_thesis: verum
end;
caseA6: a in Ball (x2,r2) ; ::_thesis: a in Ball (x,r)
then  dist (x2,a) < r2 by METRIC_1:11;
then  (dist (x2,a)) - (abs r2) < r2 - r2 by ABSVALUE:4, XREAL_1:14;
then  ( dist (x,a) <= (dist (x1,x2)) + (dist (x2,a)) & ((dist (x2,a)) - (abs r2)) + (abs r2) < 0 + (abs r2) ) by METRIC_1:4, XREAL_1:8;
then  (dist (x,a)) - (abs r2) < ((dist (x1,x2)) + (dist (x2,a))) - (dist (x2,a)) by XREAL_1:15;
then  ((dist (x,a)) - (abs r2)) - (abs r1) < (dist (x1,x2)) - 0 by COMPLEX1:46, XREAL_1:14;
then A7: ((dist (x,a)) - ((abs r1) + (abs r2))) + ((abs r1) + (abs r2)) < ((abs r1) + (abs r2)) + (dist (x1,x2)) by XREAL_1:8;
 not M is empty by A6;
hence  a in Ball (x,r) by A7, METRIC_1:11; ::_thesis: verum
end;
end;
end;
hence  a in Ball (x,r) ; ::_thesis: verum
end;
hence  (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by TARSKI:def_3; ::_thesis: verum
end;

theorem Th2: :: WEIERSTR:2
for M being MetrSpace
for n being Nat
for F being Subset-Family of M
for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
proof
let M be MetrSpace; ::_thesis: for n being Nat
for F being Subset-Family of M
for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
let n be Nat; ::_thesis: for F being Subset-Family of M
for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
let F be Subset-Family of M; ::_thesis: for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
let p be FinSequence; ::_thesis: ( F is being_ball-family & rng p = F & dom p = Seg (n + 1) implies ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) )
assume that
A1: F is being_ball-family and
A2: rng p = F and
A3: dom p = Seg (n + 1) ; ::_thesis: ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
 n + 1 in dom p by A3, FINSEQ_1:4;
then  p . (n + 1) in F by A2, FUNCT_1:def_3;
then consider x being Point of M such that
A4: ex r being Real st p . (n + 1) = Ball (x,r) by A1, TOPMETR:def_4;
consider r being Real such that
A5: p . (n + 1) = Ball (x,r) by A4;
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
A6: rng q c= rng p by RELAT_1:70;
then reconsider G = rng q as Subset-Family of M by A2, XBOOLE_1:1;
reconsider G = G as Subset-Family of M ;
 len p = n + 1 by A3, FINSEQ_1:def_3;
then  n <= len p by NAT_1:11;
then A7: dom q = Seg n by FINSEQ_1:17;
then A8: (dom q) \/ {(n + 1)} = dom p by A3, FINSEQ_1:9;
A9: ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r))
proof
take  x ; ::_thesis: ex r being Real st union F c= (union G) \/ (Ball (x,r))
take  r ; ::_thesis: union F c= (union G) \/ (Ball (x,r))
 union F c= (union G) \/ (Ball (x,r))
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in union F or t in (union G) \/ (Ball (x,r)) )
assume  t in union F ; ::_thesis: t in (union G) \/ (Ball (x,r))
then consider A being set  such that
A10: t in A and
A11: A in F by TARSKI:def_4;
consider s being set  such that
A12: s in dom p and
A13: A = p . s by A2, A11, FUNCT_1:def_3;
now__::_thesis:_(_(_s_in_dom_q_&_t_in_(union_G)_\/_(Ball_(x,r))_)_or_(_s_in_{(n_+_1)}_&_t_in_(union_G)_\/_(Ball_(x,r))_)_)
percases ( s in dom q or s in {(n + 1)} ) by A8, A12, XBOOLE_0:def_3;
case s in dom q ; ::_thesis: t in (union G) \/ (Ball (x,r))
then  ( q . s in G & q . s = A ) by A13, FUNCT_1:47, FUNCT_1:def_3;
then A14: t in union G by A10, TARSKI:def_4;
 union G c= (union G) \/ (Ball (x,r)) by XBOOLE_1:7;
hence  t in (union G) \/ (Ball (x,r)) by A14; ::_thesis: verum
end;
case s in {(n + 1)} ; ::_thesis: t in (union G) \/ (Ball (x,r))
then  p . s = Ball (x,r) by A5, TARSKI:def_1;
hence  t in (union G) \/ (Ball (x,r)) by A10, A13, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  t in (union G) \/ (Ball (x,r)) ; ::_thesis: verum
end;
hence  union F c= (union G) \/ (Ball (x,r)) ; ::_thesis: verum
end;
take  G ; ::_thesis: ( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
 for x being set st x in G holds
ex y being Point of M ex r being Real st x = Ball (y,r) by A1, A2, A6, TOPMETR:def_4;
hence  ( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) by A7, A9, TOPMETR:def_4; ::_thesis: verum
end;

theorem Th3: :: WEIERSTR:3
for M being MetrSpace
for F being Subset-Family of M st F is finite & F is being_ball-family holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
proof
let M be MetrSpace; ::_thesis: for F being Subset-Family of M st F is finite & F is being_ball-family holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
let F be Subset-Family of M; ::_thesis: ( F is finite & F is being_ball-family implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )
assume that
A1: F is finite and
A2: F is being_ball-family ; ::_thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)
consider p being FinSequence such that
A3: rng p = F by A1, FINSEQ_1:52;
A4: for F being Subset-Family of M st F is finite & F is being_ball-family holds
for n being Nat
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
proof
defpred S1[ Nat] means  for F being Subset-Family of M st F is finite & F is being_ball-family holds
for n being Nat st n = $1 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r);
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; ::_thesis: S1[k + 1]
let F be Subset-Family of M; ::_thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = k + 1 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r) )
assume that
 F is finite and
A7: F is being_ball-family ; ::_thesis: for n being Nat st n = k + 1 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
let n be Nat; ::_thesis: ( n = k + 1 implies for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r) )
assume A8: n = k + 1 ; ::_thesis: for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
let p be FinSequence; ::_thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )
assume  ( rng p = F & dom p = Seg n ) ; ::_thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)
then consider F1 being Subset-Family of M such that
A9: ( F1 is finite & F1 is being_ball-family ) and
A10: ex p1 being FinSequence st
( rng p1 = F1 & dom p1 = Seg k & ex x2 being Point of M ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) ) by A7, A8, Th2;
consider x1 being Point of M such that
A11: ex r being Real st union F1 c= Ball (x1,r) by A6, A9, A10;
consider x2 being Point of M such that
A12: ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) by A10;
consider r2 being Real such that
A13: union F c= (union F1) \/ (Ball (x2,r2)) by A12;
consider r1 being Real such that
A14: union F1 c= Ball (x1,r1) by A11;
consider x being Point of M such that
A15: ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by Th1;
take  x ; ::_thesis: ex r being Real st union F c= Ball (x,r)
consider r being Real such that
A16: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by A15;
take  r ; ::_thesis: union F c= Ball (x,r)
 (union F1) \/ (Ball (x2,r2)) c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A14, XBOOLE_1:9;
then  union F c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A13, XBOOLE_1:1;
hence  union F c= Ball (x,r) by A16, XBOOLE_1:1; ::_thesis: verum
end;
A17: S1[ 0 ]
proof
let F be Subset-Family of M; ::_thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = 0 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r) )
assume that
 F is finite and
 F is being_ball-family ; ::_thesis: for n being Nat st n = 0 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
let n be Nat; ::_thesis: ( n = 0 implies for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r) )
assume  n = 0 ; ::_thesis: for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
then A18: Seg n = {} ;
 for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
proof
set x = the Point of M;
let p be FinSequence; ::_thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )
assume A19: ( rng p = F & dom p = Seg n ) ; ::_thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)
take  the Point of M ; ::_thesis: ex r being Real st union F c= Ball ( the Point of M,r)
take  0 ; ::_thesis: union F c= Ball ( the Point of M,0)
 union F = {} by A19, A18, RELAT_1:42, ZFMISC_1:2;
hence  union F c= Ball ( the Point of M,0) by XBOOLE_1:2; ::_thesis: verum
end;
hence  for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r) ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A17, A5);
hence  for F being Subset-Family of M st F is finite & F is being_ball-family holds
for n being Nat
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball (x,r) ; ::_thesis: verum
end;
 ex n being Nat st dom p = Seg n by FINSEQ_1:def_2;
hence  ex x being Point of M ex r being Real st union F c= Ball (x,r) by A2, A4, A3; ::_thesis: verum
end;

theorem Th4: :: WEIERSTR:4
for T, S being non empty TopSpace
for f being Function of T,S
for B being Subset-Family of S st f is continuous & B is open holds
f " B is open
proof
let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S
for B being Subset-Family of S st f is continuous & B is open holds
f " B is open
let f be Function of T,S; ::_thesis: for B being Subset-Family of S st f is continuous & B is open holds
f " B is open
let B be Subset-Family of S; ::_thesis: ( f is continuous & B is open implies f " B is open )
assume that
A1: f is continuous and
A2: B is open ; ::_thesis: f " B is open
 for P being Subset of T st P in f " B holds
P is open
proof
let P be Subset of T; ::_thesis: ( P in f " B implies P is open )
assume A3: P in f " B ; ::_thesis: P is open
thus  P is open ::_thesis: verum
proof
consider C being Subset of S such that
A4: C in B and
A5: P = f " C by A3, FUNCT_2:def_9;
reconsider C = C as Subset of S ;
 ( [#] S <> {} & C is open ) by A2, A4, TOPS_2:def_1;
hence  P is open by A1, A5, TOPS_2:43; ::_thesis: verum
end;
end;
hence  f " B is open by TOPS_2:def_1; ::_thesis: verum
end;

theorem :: WEIERSTR:5
for T, S being non empty TopSpace
for f being Function of T,S
for Q being Subset-Family of S st Q is finite holds
f " Q is finite
proof
let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S
for Q being Subset-Family of S st Q is finite holds
f " Q is finite
let f be Function of T,S; ::_thesis: for Q being Subset-Family of S st Q is finite holds
f " Q is finite
let Q be Subset-Family of S; ::_thesis: ( Q is finite implies f " Q is finite )
defpred S1[ Subset of ([#] S), Subset of ([#] T)] means  for s, t being set st $1 = s & $2 = t holds
t = f " s;
assume  Q is finite ; ::_thesis: f " Q is finite
then consider s being FinSequence such that
A1: rng s = Q by FINSEQ_1:52;
A2: for x being Subset of ([#] S) ex y being Subset of ([#] T) st S1[x,y]
proof
let x be Subset of ([#] S); ::_thesis: ex y being Subset of ([#] T) st S1[x,y]
reconsider x = x as set ;
set y = f " x;
reconsider y = f " x as Subset of ([#] T) ;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider F being Function of (bool ([#] S)),(bool ([#] T)) such that
A3: for x being Subset of ([#] S) holds S1[x,F . x] from FUNCT_2:sch_3(A2);
 dom F = bool ([#] S) by FUNCT_2:def_1;
then reconsider q = F * s as FinSequence by A1, FINSEQ_1:16;
 for x being set holds
( x in F .: Q iff x in f " Q )
proof
let x be set ; ::_thesis: ( x in F .: Q iff x in f " Q )
A4: dom F = bool ([#] S) by FUNCT_2:def_1;
thus  ( x in F .: Q implies x in f " Q ) ::_thesis: ( x in f " Q implies x in F .: Q )
proof
assume  x in F .: Q ; ::_thesis: x in f " Q
then consider y being set  such that
A5: y in dom F and
A6: ( y in Q & x = F . y ) by FUNCT_1:def_6;
reconsider y = y as Subset of S by A5;
 F . y = f " y by A3;
hence  x in f " Q by A6, FUNCT_2:def_9; ::_thesis: verum
end;
assume A7: x in f " Q ; ::_thesis: x in F .: Q
then reconsider x = x as Subset of T ;
consider y being Subset of S such that
A8: y in Q and
A9: x = f " y by A7, FUNCT_2:def_9;
 x = F . y by A3, A9;
hence  x in F .: Q by A8, A4, FUNCT_1:def_6; ::_thesis: verum
end;
then A10: F .: Q = f " Q by TARSKI:1;
 ex q being FinSequence st rng q = f " Q
proof
take  q ; ::_thesis: rng q = f " Q
thus  rng q = f " Q by A1, A10, RELAT_1:127; ::_thesis: verum
end;
hence  f " Q is finite ; ::_thesis: verum
end;

theorem :: WEIERSTR:6
for T, S being non empty TopSpace
for f being Function of T,S
for P being Subset-Family of T st P is finite holds
f .: P is finite
proof
let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S
for P being Subset-Family of T st P is finite holds
f .: P is finite
let f be Function of T,S; ::_thesis: for P being Subset-Family of T st P is finite holds
f .: P is finite
let P be Subset-Family of T; ::_thesis: ( P is finite implies f .: P is finite )
defpred S1[ Subset of ([#] T), Subset of ([#] S)] means  for s, t being set st $1 = s & $2 = t holds
t = f .: s;
assume  P is finite ; ::_thesis: f .: P is finite
then consider s being FinSequence such that
A1: rng s = P by FINSEQ_1:52;
A2: for x being Subset of ([#] T) ex y being Subset of ([#] S) st S1[x,y]
proof
let x be Subset of ([#] T); ::_thesis: ex y being Subset of ([#] S) st S1[x,y]
reconsider x = x as set ;
set y = f .: x;
reconsider y = f .: x as Subset of ([#] S) ;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider F being Function of (bool ([#] T)),(bool ([#] S)) such that
A3: for x being Subset of ([#] T) holds S1[x,F . x] from FUNCT_2:sch_3(A2);
 dom F = bool ([#] T) by FUNCT_2:def_1;
then reconsider q = F * s as FinSequence by A1, FINSEQ_1:16;
 for x being set holds
( x in F .: P iff x in f .: P )
proof
let x be set ; ::_thesis: ( x in F .: P iff x in f .: P )
thus  ( x in F .: P implies x in f .: P ) ::_thesis: ( x in f .: P implies x in F .: P )
proof
assume  x in F .: P ; ::_thesis: x in f .: P
then consider y being set  such that
A4: y in dom F and
A5: ( y in P & x = F . y ) by FUNCT_1:def_6;
reconsider y = y as Subset of T by A4;
 F . y = f .: y by A3;
hence  x in f .: P by A5, FUNCT_2:def_10; ::_thesis: verum
end;
thus  ( x in f .: P implies x in F .: P ) ::_thesis: verum
proof
assume A6: x in f .: P ; ::_thesis: x in F .: P
then reconsider x = x as Subset of S ;
consider y being Subset of T such that
A7: y in P and
A8: x = f .: y by A6, FUNCT_2:def_10;
A9: dom F = bool ([#] T) by FUNCT_2:def_1;
 x = F . y by A3, A8;
hence  x in F .: P by A7, A9, FUNCT_1:def_6; ::_thesis: verum
end;
end;
then A10: F .: P = f .: P by TARSKI:1;
 ex q being FinSequence st rng q = f .: P
proof
take  q ; ::_thesis: rng q = f .: P
thus  rng q = f .: P by A1, A10, RELAT_1:127; ::_thesis: verum
end;
hence  f .: P is finite ; ::_thesis: verum
end;

theorem Th7: :: WEIERSTR:7
for T, S being non empty TopSpace
for f being Function of T,S
for P being Subset of T
for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
proof
let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S
for P being Subset of T
for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
let f be Function of T,S; ::_thesis: for P being Subset of T
for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
let P be Subset of T; ::_thesis: for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
let F be Subset-Family of S; ::_thesis: ( ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) implies ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) )
given B being Subset-Family of T such that A1: B c= f " F and
A2: B is Cover of P and
A3: B is finite ; ::_thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
A4: P c= union B by A2, SETFAM_1:def_11;
now__::_thesis:_(_(_P_<>_{}_&_ex_G_being_Subset-Family_of_S_st_
(_G_c=_F_&_G_is_Cover_of_f_.:_P_&_G_is_finite_)_&_ex_G_being_Subset-Family_of_S_st_
(_G_c=_F_&_G_is_Cover_of_f_.:_P_&_G_is_finite_)_)_or_(_P_=_{}_&_ex_G_being_Subset-Family_of_S_st_
(_G_c=_F_&_G_is_Cover_of_f_.:_P_&_G_is_finite_)_)_)
percases ( P <> {} or P = {} ) ;
caseA5: P <> {} ; ::_thesis: ( ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) & ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) )
thus  ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) ::_thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
proof
consider s being FinSequence such that
A6: rng s = B by A3, FINSEQ_1:52;
 B <> {} by A4, A5, ZFMISC_1:2;
then consider D being non empty set  such that
A7: D = B ;
defpred S1[ Element of D, Subset of ([#] S)] means  for x being Element of D st $1 = x holds
for y being Subset of ([#] S) st $2 = y holds
( y in F & x = f " y );
A8: for x being Element of D ex y being Subset of ([#] S) st S1[x,y]
proof
let x be Element of D; ::_thesis: ex y being Subset of ([#] S) st S1[x,y]
A9: x in B by A7;
then reconsider x = x as Subset of T ;
consider y being Subset of S such that
A10: ( y in F & x = f " y ) by A1, A9, FUNCT_2:def_9;
reconsider y = y as Subset of ([#] S) ;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] by A10; ::_thesis: verum
end;
consider F0 being Function of D,(bool ([#] S)) such that
A11: for x being Element of D holds S1[x,F0 . x] from FUNCT_2:sch_3(A8);
A12: for x being Element of D holds
( F0 . x in F & x = f " (F0 . x) ) by A11;
reconsider F0 = F0 as Function of B,(bool ([#] S)) by A7;
A13: dom F0 = B by FUNCT_2:def_1;
then reconsider q = F0 * s as FinSequence by A6, FINSEQ_1:16;
set G = rng q;
A14: rng q c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q or x in F )
assume  x in rng q ; ::_thesis: x in F
then consider y being set  such that
A15: ( y in dom q & x = q . y ) by FUNCT_1:def_3;
 ( s . y in B & x = F0 . (s . y) ) by A13, A15, FUNCT_1:11, FUNCT_1:12;
hence  x in F by A7, A12; ::_thesis: verum
end;
then reconsider G = rng q as Subset-Family of S by XBOOLE_1:1;
reconsider G = G as Subset-Family of S ;
take  G ; ::_thesis: ( G c= F & G is Cover of f .: P & G is finite )
 for x being set st x in f .: P holds
x in union G
proof
let x be set ; ::_thesis: ( x in f .: P implies x in union G )
assume A16: x in f .: P ; ::_thesis: x in union G
 ex A being set st
( x in A & A in G )
proof
consider y being set  such that
A17: y in dom f and
A18: y in P and
A19: x = f . y by A16, FUNCT_1:def_6;
consider C being set  such that
A20: y in C and
A21: C in B by A4, A18, TARSKI:def_4;
 C = f " (F0 . C) by A7, A12, A21;
then A22: x in f .: (f " (F0 . C)) by A17, A19, A20, FUNCT_1:def_6;
set A = F0 . C;
take  F0 . C ; ::_thesis: ( x in F0 . C & F0 . C in G )
 ( f .: (f " (F0 . C)) c= F0 . C & G = rng F0 ) by A6, A13, FUNCT_1:75, RELAT_1:28;
hence  ( x in F0 . C & F0 . C in G ) by A21, A22, FUNCT_2:4; ::_thesis: verum
end;
hence  x in union G by TARSKI:def_4; ::_thesis: verum
end;
then  f .: P c= union G by TARSKI:def_3;
hence  ( G c= F & G is Cover of f .: P & G is finite ) by A14, SETFAM_1:def_11; ::_thesis: verum
end;
hence  ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) ; ::_thesis: verum
end;
caseA23: P = {} ; ::_thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
 ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
proof
set G = {} ;
reconsider G = {} as Subset-Family of S by XBOOLE_1:2;
reconsider G = G as Subset-Family of S ;
take  G ; ::_thesis: ( G c= F & G is Cover of f .: P & G is finite )
 f .: P = {}
proof
assume  f .: P <> {} ; ::_thesis: contradiction
then consider x being set  such that
A24: x in f .: P by XBOOLE_0:def_1;
 ex z being set st
( z in dom f & z in P & x = f . z ) by A24, FUNCT_1:def_6;
hence  contradiction by A23; ::_thesis: verum
end;
hence  ( G c= F & G is Cover of f .: P & G is finite ) by SETFAM_1:def_11, XBOOLE_1:2, ZFMISC_1:2; ::_thesis: verum
end;
hence  ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) ; ::_thesis: verum
end;
end;
end;
hence  ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) ; ::_thesis: verum
end;

begin

theorem Th8: :: WEIERSTR:8
for T, S being non empty TopSpace
for f being Function of T,S
for P being Subset of T st P is compact & f is continuous holds
f .: P is compact
proof
let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S
for P being Subset of T st P is compact & f is continuous holds
f .: P is compact
let f be Function of T,S; ::_thesis: for P being Subset of T st P is compact & f is continuous holds
f .: P is compact
let P be Subset of T; ::_thesis: ( P is compact & f is continuous implies f .: P is compact )
assume that
A1: P is compact and
A2: f is continuous ; ::_thesis: f .: P is compact
 P c= [#] T ;
then A3: P c= dom f by FUNCT_2:def_1;
 for F0 being Subset-Family of S st F0 is Cover of f .: P & F0 is open holds
ex G being Subset-Family of S st
( G c= F0 & G is Cover of f .: P & G is finite )
proof
let F0 be Subset-Family of S; ::_thesis: ( F0 is Cover of f .: P & F0 is open implies ex G being Subset-Family of S st
( G c= F0 & G is Cover of f .: P & G is finite ) )
assume that
A4: F0 is Cover of f .: P and
A5: F0 is open ; ::_thesis: ex G being Subset-Family of S st
( G c= F0 & G is Cover of f .: P & G is finite )
set B0 = f " F0;
A6: f .: P c= union F0 by A4, SETFAM_1:def_11;
 P c= union (f " F0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in union (f " F0) )
thus  ( x in P implies x in union (f " F0) ) ::_thesis: verum
proof
A7: f " (union F0) c= union (f " F0)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f " (union F0) or y in union (f " F0) )
assume A8: y in f " (union F0) ; ::_thesis: y in union (f " F0)
thus  y in union (f " F0) ::_thesis: verum
proof
 f . y in union F0 by A8, FUNCT_1:def_7;
then consider Q being set  such that
A9: ( f . y in Q & Q in F0 ) by TARSKI:def_4;
A10: y in dom f by A8, FUNCT_1:def_7;
 ex Z being set st
( y in Z & Z in f " F0 )
proof
set Z = f " Q;
take  f " Q ; ::_thesis: ( y in f " Q & f " Q in f " F0 )
thus  ( y in f " Q & f " Q in f " F0 ) by A10, A9, FUNCT_1:def_7, FUNCT_2:def_9; ::_thesis: verum
end;
hence  y in union (f " F0) by TARSKI:def_4; ::_thesis: verum
end;
end;
assume A11: x in P ; ::_thesis: x in union (f " F0)
then A12: f . x in f .: P by A3, FUNCT_1:def_6;
reconsider x = x as Point of T by A11;
A13: f . x in union F0 by A6, A12;
A14: f " {(f . x)} c= f " (union F0)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f " {(f . x)} or y in f " (union F0) )
assume A15: y in f " {(f . x)} ; ::_thesis: y in f " (union F0)
then  f . y in {(f . x)} by FUNCT_1:def_7;
then A16: f . y in union F0 by A13, TARSKI:def_1;
 y in dom f by A15, FUNCT_1:def_7;
hence  y in f " (union F0) by A16, FUNCT_1:def_7; ::_thesis: verum
end;
 f . x in {(f . x)} by TARSKI:def_1;
then  x in f " {(f . x)} by A3, A11, FUNCT_1:def_7;
then  x in f " (union F0) by A14;
hence  x in union (f " F0) by A7; ::_thesis: verum
end;
end;
then A17: f " F0 is Cover of P by SETFAM_1:def_11;
 f " F0 is open by A2, A5, Th4;
then  ex B being Subset-Family of T st
( B c= f " F0 & B is Cover of P & B is finite ) by A1, A17, COMPTS_1:def_4;
then consider G being Subset-Family of S such that
A18: ( G c= F0 & G is Cover of f .: P & G is finite ) by Th7;
take  G ; ::_thesis: ( G c= F0 & G is Cover of f .: P & G is finite )
thus  ( G c= F0 & G is Cover of f .: P & G is finite ) by A18; ::_thesis: verum
end;
hence  f .: P is compact by COMPTS_1:def_4; ::_thesis: verum
end;

theorem :: WEIERSTR:9
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P is compact & f is continuous holds
f .: P is compact by Th8;

theorem :: WEIERSTR:10
for f being Function of (TOP-REAL 2),R^1
for P being Subset of (TOP-REAL 2) st P is compact & f is continuous holds
f .: P is compact by Th8;

definition
let P be Subset of R^1;
func [#] P ->  Subset of REAL equals :: WEIERSTR:def 1
P;
correctness
coherence
P is Subset of REAL;
by TOPMETR:17;
end;

:: deftheorem  defines [#] WEIERSTR:def_1_:_
 for P being Subset of R^1 holds [#] P = P;

theorem Th11: :: WEIERSTR:11
for P being Subset of R^1 st P is compact holds
[#] P is real-bounded
proof
let P be Subset of R^1; ::_thesis: ( P is compact implies [#] P is real-bounded )
assume A1: P is compact ; ::_thesis: [#] P is real-bounded
thus  [#] P is real-bounded ::_thesis: verum
proof
now__::_thesis:_(_(_[#]_P_<>_{}_&_[#]_P_is_real-bounded_)_or_(_[#]_P_=_{}_&_[#]_P_is_real-bounded_)_)
percases ( [#] P <> {} or [#] P = {} ) ;
case [#] P <> {} ; ::_thesis: [#] P is real-bounded
set r0 = 1;
defpred S1[ Subset of R^1] means  ex x being Point of RealSpace st
( x in [#] P & $1 = Ball (x,1) );
consider R being Subset-Family of R^1 such that
A2: for A being Subset of R^1 holds
( A in R iff S1[A] ) from SUBSET_1:sch_3();
 for x being set st x in [#] P holds
x in union R
proof
let x be set ; ::_thesis: ( x in [#] P implies x in union R )
assume A3: x in [#] P ; ::_thesis: x in union R
then reconsider x = x as Point of RealSpace by METRIC_1:def_13;
consider A being Subset of RealSpace such that
A4: A = Ball (x,1) ;
 R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def_5, TOPMETR:def_6;
then reconsider A = A as Subset of R^1 ;
 ex A being set st
( x in A & A in R )
proof
take  A ; ::_thesis: ( x in A & A in R )
 dist (x,x) = 0 by METRIC_1:1;
hence  ( x in A & A in R ) by A2, A3, A4, METRIC_1:11; ::_thesis: verum
end;
hence  x in union R by TARSKI:def_4; ::_thesis: verum
end;
then  [#] P c= union R by TARSKI:def_3;
then A5: R is Cover of P by SETFAM_1:def_11;
 for A being Subset of R^1 st A in R holds
A is open
proof
let A be Subset of R^1; ::_thesis: ( A in R implies A is open )
assume  A in R ; ::_thesis: A is open
then  ex x being Point of RealSpace st
( x in [#] P & A = Ball (x,1) ) by A2;
hence  A is open by TOPMETR:14, TOPMETR:def_6; ::_thesis: verum
end;
then  R is open by TOPS_2:def_1;
then consider R0 being Subset-Family of R^1 such that
A6: R0 c= R and
A7: R0 is Cover of P and
A8: R0 is finite by A1, A5, COMPTS_1:def_4;
A9: P c= union R0 by A7, SETFAM_1:def_11;
A10: for A being set st A in R0 holds
ex x being Point of RealSpace ex r being Real st A = Ball (x,r)
proof
let A be set ; ::_thesis: ( A in R0 implies ex x being Point of RealSpace ex r being Real st A = Ball (x,r) )
assume A11: A in R0 ; ::_thesis: ex x being Point of RealSpace ex r being Real st A = Ball (x,r)
then reconsider A = A as Subset of R^1 ;
consider x being Point of RealSpace such that
 x in [#] P and
A12: A = Ball (x,1) by A2, A6, A11;
take  x ; ::_thesis: ex r being Real st A = Ball (x,r)
take  1 ; ::_thesis: A = Ball (x,1)
thus  A = Ball (x,1) by A12; ::_thesis: verum
end;
 R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def_5, TOPMETR:def_6;
then reconsider R0 = R0 as Subset-Family of RealSpace ;
 R0 is being_ball-family by A10, TOPMETR:def_4;
then consider x1 being Point of RealSpace such that
A13: ex r1 being Real st union R0 c= Ball (x1,r1) by A8, Th3;
consider r1 being Real such that
A14: union R0 c= Ball (x1,r1) by A13;
A15: [#] P c= Ball (x1,r1) by A9, A14, XBOOLE_1:1;
reconsider x1 = x1 as Real by METRIC_1:def_13;
A16: for p being Real st p in [#] P holds
( x1 - r1 <= p & p <= x1 + r1 )
proof
let p be Real; ::_thesis: ( p in [#] P implies ( x1 - r1 <= p & p <= x1 + r1 ) )
reconsider a = x1, b = p as Element of RealSpace by METRIC_1:def_13;
assume  p in [#] P ; ::_thesis: ( x1 - r1 <= p & p <= x1 + r1 )
then  dist (a,b) < r1 by A15, METRIC_1:11;
then A17: abs (x1 - p) < r1 by TOPMETR:11;
then  - r1 <= x1 - p by ABSVALUE:5;
then  (- r1) + p <= x1 by XREAL_1:19;
then A18: p <= x1 - (- r1) by XREAL_1:19;
 x1 - p <= r1 by A17, ABSVALUE:5;
then  x1 <= p + r1 by XREAL_1:20;
hence  ( x1 - r1 <= p & p <= x1 + r1 ) by A18, XREAL_1:20; ::_thesis: verum
end;
 x1 - r1 is LowerBound of [#] P
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in [#] P or x1 - r1 <= r )
thus  ( not r in [#] P or x1 - r1 <= r ) by A16; ::_thesis: verum
end;
then A19: [#] P is bounded_below by XXREAL_2:def_9;
 x1 + r1 is UpperBound of [#] P
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in [#] P or r <= x1 + r1 )
thus  ( not r in [#] P or r <= x1 + r1 ) by A16; ::_thesis: verum
end;
then  [#] P is bounded_above by XXREAL_2:def_10;
hence  [#] P is real-bounded by A19, XXREAL_2:def_11; ::_thesis: verum
end;
caseA20: [#] P = {} ; ::_thesis: [#] P is real-bounded
 0 is LowerBound of [#] P
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in [#] P or 0 <= r )
thus  ( not r in [#] P or 0 <= r ) by A20; ::_thesis: verum
end;
then A21: [#] P is bounded_below by XXREAL_2:def_9;
 0 is UpperBound of [#] P
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in [#] P or r <= 0 )
thus  ( not r in [#] P or r <= 0 ) by A20; ::_thesis: verum
end;
then  [#] P is bounded_above by XXREAL_2:def_10;
hence  [#] P is real-bounded by A21, XXREAL_2:def_11; ::_thesis: verum
end;
end;
end;
hence  [#] P is real-bounded ; ::_thesis: verum
end;
end;

theorem Th12: :: WEIERSTR:12
for P being Subset of R^1 st P is compact holds
[#] P is closed
proof
let P be Subset of R^1; ::_thesis: ( P is compact implies [#] P is closed )
assume A1: P is compact ; ::_thesis: [#] P is closed
now__::_thesis:_(_(_[#]_P_<>_{}_&_[#]_P_is_closed_)_or_(_[#]_P_=_{}_&_[#]_P_is_closed_)_)
percases ( [#] P <> {} or [#] P = {} ) ;
caseA2: [#] P <> {} ; ::_thesis: [#] P is closed
A3: R^1 is T_2 by PCOMPS_1:34, TOPMETR:def_6;
 for s1 being Real_Sequence st rng s1 c= [#] P & s1 is convergent holds
lim s1 in [#] P
proof
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [#] P & s1 is convergent implies lim s1 in [#] P )
assume that
A4: rng s1 c= [#] P and
A5: s1 is convergent ; ::_thesis: lim s1 in [#] P
set x = lim s1;
reconsider x = lim s1 as Point of R^1 by TOPMETR:17;
thus  lim s1 in [#] P ::_thesis: verum
proof
assume  not lim s1 in [#] P ; ::_thesis: contradiction
then  x in P ` by SUBSET_1:29;
then consider Otx, OtP being Subset of R^1 such that
A6: Otx is open and
 OtP is open and
A7: x in Otx and
A8: ( P c= OtP & Otx misses OtP ) by A1, A2, A3, COMPTS_1:6;
A9: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def_5, TOPMETR:def_6;
then reconsider x = x as Point of RealSpace ;
consider r being real number  such that
A10: r > 0 and
A11: Ball (x,r) c= Otx by A6, A7, TOPMETR:15, TOPMETR:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A12: Ball (x,r) =  {  q where q is Element of RealSpace : dist (x,q) < r  }  by METRIC_1:17;
 rng s1 misses Otx by A4, A8, XBOOLE_1:1, XBOOLE_1:63;
then A13: Ball (x,r) misses rng s1 by A11, XBOOLE_1:63;
 for n being Element of NAT ex m being Element of NAT st
( n <= m & not abs ((s1 . m) - (lim s1)) < r )
proof
given n being Element of NAT  such that A14: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < r ; ::_thesis: contradiction
set m = n + 1;
 abs ((s1 . (n + 1)) - (lim s1)) < r by A14, NAT_1:11;
then  real_dist . ((s1 . (n + 1)),(lim s1)) < r by METRIC_1:def_12;
then A15: real_dist . ((lim s1),(s1 . (n + 1))) < r by METRIC_1:9;
reconsider y = s1 . (n + 1) as Element of RealSpace by A9, TOPMETR:17;
A16: s1 . (n + 1) in rng s1 by FUNCT_2:4;
 dist (x,y) = the distance of RealSpace . (x,y) by METRIC_1:def_1;
then  y in Ball (x,r) by A12, A15, METRIC_1:def_13;
then  y in (Ball (x,r)) /\ (rng s1) by A16, XBOOLE_0:def_4;
hence  contradiction by A13, XBOOLE_0:def_7; ::_thesis: verum
end;
hence  contradiction by A5, A10, SEQ_2:def_7; ::_thesis: verum
end;
end;
hence  [#] P is closed by RCOMP_1:def_4; ::_thesis: verum
end;
caseA17: [#] P = {} ; ::_thesis: [#] P is closed
 for s1 being Real_Sequence st rng s1 c= [#] P & s1 is convergent holds
lim s1 in [#] P
proof
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [#] P & s1 is convergent implies lim s1 in [#] P )
assume that
A18: rng s1 c= [#] P and
 s1 is convergent ; ::_thesis: lim s1 in [#] P
 ex x being set st x in NAT by XBOOLE_0:def_1;
hence  lim s1 in [#] P by A17, A18, FUNCT_2:4; ::_thesis: verum
end;
hence  [#] P is closed by RCOMP_1:def_4; ::_thesis: verum
end;
end;
end;
hence  [#] P is closed ; ::_thesis: verum
end;

theorem Th13: :: WEIERSTR:13
for P being Subset of R^1 st P is compact holds
[#] P is compact
proof
let P be Subset of R^1; ::_thesis: ( P is compact implies [#] P is compact )
assume A1: P is compact ; ::_thesis: [#] P is compact
now__::_thesis:_(_(_[#]_P_<>_{}_&_[#]_P_is_compact_)_or_(_[#]_P_=_{}_&_(_not_[#]_P_is_compact_implies_[#]_P_is_compact_)_)_)
percases ( [#] P <> {} or [#] P = {} ) ;
case [#] P <> {} ; ::_thesis: [#] P is compact
 [#] P is real-bounded by A1, Th11;
hence  [#] P is compact by A1, Th12, RCOMP_1:11; ::_thesis: verum
end;
caseA2: [#] P = {} ; ::_thesis: ( not [#] P is compact implies [#] P is compact )
assume  not [#] P is compact ; ::_thesis: [#] P is compact
then A3: ex s1 being Real_Sequence st
( rng s1 c= [#] P & ( for s2 being Real_Sequence holds
( not s2 is subsequence of s1 or not s2 is convergent or not lim s2 in [#] P ) ) ) by RCOMP_1:def_3;
 ex x being set st x in NAT by XBOOLE_0:def_1;
hence  [#] P is compact by A2, A3, FUNCT_2:4; ::_thesis: verum
end;
end;
end;
hence  [#] P is compact ; ::_thesis: verum
end;

Lm1:  for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
let f be Function of T,R^1; ::_thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
let P be Subset of T; ::_thesis: ( P <> {} & P is compact & f is continuous implies ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) )
assume that
A1: P <> {} and
A2: ( P is compact & f is continuous ) ; ::_thesis: ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
A3: [#] (f .: P) <> {}
proof
consider x being set  such that
A4: x in P by A1, XBOOLE_0:def_1;
 dom f = the carrier of T by FUNCT_2:def_1;
then  f . x in f .: P by A4, FUNCT_1:def_6;
hence  [#] (f .: P) <> {} ; ::_thesis: verum
end;
consider y1, y2 being Real such that
A5: y1 = upper_bound ([#] (f .: P)) and
A6: y2 = lower_bound ([#] (f .: P)) ;
A7: [#] (f .: P) is compact by A2, Th8, Th13;
then  y1 in [#] (f .: P) by A3, A5, RCOMP_1:14;
then consider x1 being set  such that
A8: x1 in dom f and
A9: ( x1 in P & y1 = f . x1 ) by FUNCT_1:def_6;
 y2 in [#] (f .: P) by A3, A6, A7, RCOMP_1:14;
then consider x2 being set  such that
A10: x2 in dom f and
A11: ( x2 in P & y2 = f . x2 ) by FUNCT_1:def_6;
reconsider x1 = x1, x2 = x2 as Point of T by A8, A10;
take  x1 ; ::_thesis: ex x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
take  x2 ; ::_thesis: ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
thus  ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) by A5, A6, A9, A11; ::_thesis: verum
end;

definition
let P be Subset of R^1;
func upper_bound P ->  Real equals :: WEIERSTR:def 2
 upper_bound ([#] P);
correctness
coherence
upper_bound ([#] P) is Real;
;
func lower_bound P ->  Real equals :: WEIERSTR:def 3
 lower_bound ([#] P);
correctness
coherence
lower_bound ([#] P) is Real;
;
end;

:: deftheorem  defines upper_bound WEIERSTR:def_2_:_
 for P being Subset of R^1 holds upper_bound P = upper_bound ([#] P);

:: deftheorem  defines lower_bound WEIERSTR:def_3_:_
 for P being Subset of R^1 holds lower_bound P = lower_bound ([#] P);

theorem Th14: :: WEIERSTR:14
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) )
let f be Function of T,R^1; ::_thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) )
let P be Subset of T; ::_thesis: ( P <> {} & P is compact & f is continuous implies ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) ) )
assume  ( P <> {} & P is compact & f is continuous ) ; ::_thesis: ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) )
then consider x1, x2 being Point of T such that
A1: x1 in P and
 x2 in P and
A2: f . x1 = upper_bound ([#] (f .: P)) and
 f . x2 = lower_bound ([#] (f .: P)) by Lm1;
take  x1 ; ::_thesis: ( x1 in P & f . x1 = upper_bound (f .: P) )
thus  ( x1 in P & f . x1 = upper_bound (f .: P) ) by A1, A2; ::_thesis: verum
end;

theorem Th15: :: WEIERSTR:15
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x2 being Point of T st
( x2 in P & f . x2 = lower_bound (f .: P) )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x2 being Point of T st
( x2 in P & f . x2 = lower_bound (f .: P) )
let f be Function of T,R^1; ::_thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x2 being Point of T st
( x2 in P & f . x2 = lower_bound (f .: P) )
let P be Subset of T; ::_thesis: ( P <> {} & P is compact & f is continuous implies ex x2 being Point of T st
( x2 in P & f . x2 = lower_bound (f .: P) ) )
assume  ( P <> {} & P is compact & f is continuous ) ; ::_thesis: ex x2 being Point of T st
( x2 in P & f . x2 = lower_bound (f .: P) )
then consider x1, x2 being Point of T such that
 x1 in P and
A1: x2 in P and
 f . x1 = upper_bound ([#] (f .: P)) and
A2: f . x2 = lower_bound ([#] (f .: P)) by Lm1;
take  x2 ; ::_thesis: ( x2 in P & f . x2 = lower_bound (f .: P) )
thus  ( x2 in P & f . x2 = lower_bound (f .: P) ) by A1, A2; ::_thesis: verum
end;

begin

definition
let M be non empty MetrSpace;
let x be Point of M;
func dist x ->  Function of (TopSpaceMetr M),R^1 means :Def4: :: WEIERSTR:def 4
 for y being Point of M holds it . y = dist (y,x);
existence
 ex b1 being Function of (TopSpaceMetr M),R^1 st
for y being Point of M holds b1 . y = dist (y,x)
proof
defpred S1[ Element of M, Element of R^1] means  for s being Element of M
for t being Element of R^1 st $1 = s & $2 = t holds
t = dist (s,x);
A1: for s being Element of M ex t being Element of R^1 st S1[s,t]
proof
let s be Element of M; ::_thesis: ex t being Element of R^1 st S1[s,t]
consider t being Real such that
A2: t = dist (s,x) ;
reconsider t = t as Element of R^1 by TOPMETR:17;
take  t ; ::_thesis: S1[s,t]
thus  S1[s,t] by A2; ::_thesis: verum
end;
consider F being Function of the carrier of M, the carrier of R^1 such that
A3: for x being Element of M holds S1[x,F . x] from FUNCT_2:sch_3(A1);
A4: for y being Point of M holds F . y = dist (y,x) by A3;
 TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider F = F as Function of (TopSpaceMetr M),R^1 ;
take  F ; ::_thesis: for y being Point of M holds F . y = dist (y,x)
thus  for y being Point of M holds F . y = dist (y,x) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for y being Point of M holds b1 . y = dist (y,x) ) & ( for y being Point of M holds b2 . y = dist (y,x) ) holds
b1 = b2
proof
let F1, F2 be Function of (TopSpaceMetr M),R^1; ::_thesis: ( ( for y being Point of M holds F1 . y = dist (y,x) ) & ( for y being Point of M holds F2 . y = dist (y,x) ) implies F1 = F2 )
assume A5: for y being Point of M holds F1 . y = dist (y,x) ; ::_thesis: ( ex y being Point of M st not F2 . y = dist (y,x) or F1 = F2 )
assume A6: for y being Point of M holds F2 . y = dist (y,x) ; ::_thesis: F1 = F2
 for y being set st y in the carrier of (TopSpaceMetr M) holds
F1 . y = F2 . y
proof
let y be set ; ::_thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y )
A7: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
assume  y in the carrier of (TopSpaceMetr M) ; ::_thesis: F1 . y = F2 . y
then reconsider y = y as Point of M by A7;
F1 . y = dist (y,x) by A5
.= F2 . y by A6 ;
hence  F1 . y = F2 . y ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines dist WEIERSTR:def_4_:_
 for M being non empty MetrSpace
for x being Point of M
for b3 being Function of (TopSpaceMetr M),R^1 holds
( b3 = dist x iff for y being Point of M holds b3 . y = dist (y,x) );

theorem Th16: :: WEIERSTR:16
for M being non empty MetrSpace
for x being Point of M holds dist x is continuous
proof
let M be non empty MetrSpace; ::_thesis: for x being Point of M holds dist x is continuous
let x be Point of M; ::_thesis: dist x is continuous
A1: for P being Subset of R^1 st P is open holds
(dist x) " P is open
proof
let P be Subset of R^1; ::_thesis: ( P is open implies (dist x) " P is open )
assume A2: P is open ; ::_thesis: (dist x) " P is open
 for p being Point of M st p in (dist x) " P holds
ex r being real number st
( r > 0 & Ball (p,r) c= (dist x) " P )
proof
let p be Point of M; ::_thesis: ( p in (dist x) " P implies ex r being real number st
( r > 0 & Ball (p,r) c= (dist x) " P ) )
consider y being Point of RealSpace such that
A3: y = dist (p,x) by METRIC_1:def_13;
assume  p in (dist x) " P ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (dist x) " P )
then A4: (dist x) . p in P by FUNCT_1:def_7;
reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6;
 y in P by A4, A3, Def4;
then consider r being real number  such that
A5: r > 0 and
A6: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def_6;
reconsider r = r as Real by XREAL_0:def_1;
take  r ; ::_thesis: ( r > 0 & Ball (p,r) c= (dist x) " P )
 Ball (p,r) c= (dist x) " P
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball (p,r) or z in (dist x) " P )
assume A7: z in Ball (p,r) ; ::_thesis: z in (dist x) " P
then reconsider z = z as Point of M ;
consider q being Point of RealSpace such that
A8: q = dist (z,x) by METRIC_1:def_13;
 dist (p,z) < r by A7, METRIC_1:11;
then  (abs ((dist (p,x)) - (dist (z,x)))) + (dist (p,z)) < r + (dist (p,z)) by METRIC_6:1, XREAL_1:8;
then  abs ((dist (p,x)) - (dist (z,x))) < r by XREAL_1:6;
then  dist (y,q) < r by A3, A8, TOPMETR:11;
then  q in Ball (y,r) by METRIC_1:11;
then  q in P by A6;
then A9: (dist x) . z in P by A8, Def4;
 dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  dom (dist x) = the carrier of M by TOPMETR:12;
hence  z in (dist x) " P by A9, FUNCT_1:def_7; ::_thesis: verum
end;
hence  ( r > 0 & Ball (p,r) c= (dist x) " P ) by A5; ::_thesis: verum
end;
hence  (dist x) " P is open by TOPMETR:15; ::_thesis: verum
end;
 [#] R^1 <> {} ;
hence  dist x is continuous by A1, TOPS_2:43; ::_thesis: verum
end;

theorem :: WEIERSTR:17
for M being non empty MetrSpace
for x being Point of M
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in P & (dist x) . x1 = upper_bound ((dist x) .: P) ) by Th14, Th16;

theorem :: WEIERSTR:18
for M being non empty MetrSpace
for x being Point of M
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
ex x2 being Point of (TopSpaceMetr M) st
( x2 in P & (dist x) . x2 = lower_bound ((dist x) .: P) ) by Th15, Th16;

definition
let M be non empty MetrSpace;
let P be Subset of (TopSpaceMetr M);
func dist_max P ->  Function of (TopSpaceMetr M),R^1 means :Def5: :: WEIERSTR:def 5
 for x being Point of M holds it . x = upper_bound ((dist x) .: P);
existence
 ex b1 being Function of (TopSpaceMetr M),R^1 st
for x being Point of M holds b1 . x = upper_bound ((dist x) .: P)
proof
defpred S1[ Element of M, Element of R^1] means  for s being Element of M
for t being Element of R^1 st $1 = s & $2 = t holds
t = upper_bound ((dist s) .: P);
A1: for s being Element of M ex t being Element of R^1 st S1[s,t]
proof
let s be Element of M; ::_thesis: ex t being Element of R^1 st S1[s,t]
consider t being Real such that
A2: t = upper_bound ((dist s) .: P) ;
reconsider t = t as Element of R^1 by TOPMETR:17;
take  t ; ::_thesis: S1[s,t]
thus  S1[s,t] by A2; ::_thesis: verum
end;
consider F being Function of the carrier of M, the carrier of R^1 such that
A3: for x being Element of M holds S1[x,F . x] from FUNCT_2:sch_3(A1);
A4: for y being Point of M holds F . y = upper_bound ((dist y) .: P) by A3;
 TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider F = F as Function of (TopSpaceMetr M),R^1 ;
take  F ; ::_thesis: for x being Point of M holds F . x = upper_bound ((dist x) .: P)
thus  for x being Point of M holds F . x = upper_bound ((dist x) .: P) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b1 . x = upper_bound ((dist x) .: P) ) & ( for x being Point of M holds b2 . x = upper_bound ((dist x) .: P) ) holds
b1 = b2
proof
let F1, F2 be Function of (TopSpaceMetr M),R^1; ::_thesis: ( ( for x being Point of M holds F1 . x = upper_bound ((dist x) .: P) ) & ( for x being Point of M holds F2 . x = upper_bound ((dist x) .: P) ) implies F1 = F2 )
assume A5: for y being Point of M holds F1 . y = upper_bound ((dist y) .: P) ; ::_thesis: ( ex x being Point of M st not F2 . x = upper_bound ((dist x) .: P) or F1 = F2 )
assume A6: for y being Point of M holds F2 . y = upper_bound ((dist y) .: P) ; ::_thesis: F1 = F2
 for y being set st y in the carrier of (TopSpaceMetr M) holds
F1 . y = F2 . y
proof
let y be set ; ::_thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y )
A7: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
assume  y in the carrier of (TopSpaceMetr M) ; ::_thesis: F1 . y = F2 . y
then reconsider y = y as Point of M by A7;
F1 . y = upper_bound ((dist y) .: P) by A5
.= F2 . y by A6 ;
hence  F1 . y = F2 . y ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
func dist_min P ->  Function of (TopSpaceMetr M),R^1 means :Def6: :: WEIERSTR:def 6
 for x being Point of M holds it . x = lower_bound ((dist x) .: P);
existence
 ex b1 being Function of (TopSpaceMetr M),R^1 st
for x being Point of M holds b1 . x = lower_bound ((dist x) .: P)
proof
defpred S1[ Element of M, Element of R^1] means  for s being Element of M
for t being Element of R^1 st $1 = s & $2 = t holds
t = lower_bound ((dist s) .: P);
A8: for s being Element of M ex t being Element of R^1 st S1[s,t]
proof
let s be Element of M; ::_thesis: ex t being Element of R^1 st S1[s,t]
consider t being Real such that
A9: t = lower_bound ((dist s) .: P) ;
reconsider t = t as Element of R^1 by TOPMETR:17;
take  t ; ::_thesis: S1[s,t]
thus  S1[s,t] by A9; ::_thesis: verum
end;
consider F being Function of the carrier of M, the carrier of R^1 such that
A10: for x being Element of M holds S1[x,F . x] from FUNCT_2:sch_3(A8);
A11: for y being Point of M holds F . y = lower_bound ((dist y) .: P) by A10;
 TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider F = F as Function of (TopSpaceMetr M),R^1 ;
take  F ; ::_thesis: for x being Point of M holds F . x = lower_bound ((dist x) .: P)
thus  for x being Point of M holds F . x = lower_bound ((dist x) .: P) by A11; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b1 . x = lower_bound ((dist x) .: P) ) & ( for x being Point of M holds b2 . x = lower_bound ((dist x) .: P) ) holds
b1 = b2
proof
let F1, F2 be Function of (TopSpaceMetr M),R^1; ::_thesis: ( ( for x being Point of M holds F1 . x = lower_bound ((dist x) .: P) ) & ( for x being Point of M holds F2 . x = lower_bound ((dist x) .: P) ) implies F1 = F2 )
assume A12: for y being Point of M holds F1 . y = lower_bound ((dist y) .: P) ; ::_thesis: ( ex x being Point of M st not F2 . x = lower_bound ((dist x) .: P) or F1 = F2 )
assume A13: for y being Point of M holds F2 . y = lower_bound ((dist y) .: P) ; ::_thesis: F1 = F2
 for y being set st y in the carrier of (TopSpaceMetr M) holds
F1 . y = F2 . y
proof
let y be set ; ::_thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y )
A14: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
assume  y in the carrier of (TopSpaceMetr M) ; ::_thesis: F1 . y = F2 . y
then reconsider y = y as Point of M by A14;
F1 . y = lower_bound ((dist y) .: P) by A12
.= F2 . y by A13 ;
hence  F1 . y = F2 . y ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines dist_max WEIERSTR:def_5_:_
 for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for b3 being Function of (TopSpaceMetr M),R^1 holds
( b3 = dist_max P iff for x being Point of M holds b3 . x = upper_bound ((dist x) .: P) );

:: deftheorem Def6 defines dist_min WEIERSTR:def_6_:_
 for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for b3 being Function of (TopSpaceMetr M),R^1 holds
( b3 = dist_min P iff for x being Point of M holds b3 . x = lower_bound ((dist x) .: P) );

theorem Th19: :: WEIERSTR:19
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P is compact holds
for p1, p2 being Point of M st p1 in P holds
( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) )
proof
let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P is compact holds
for p1, p2 being Point of M st p1 in P holds
( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) )
let P be Subset of (TopSpaceMetr M); ::_thesis: ( P is compact implies for p1, p2 being Point of M st p1 in P holds
( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) )
assume A1: P is compact ; ::_thesis: for p1, p2 being Point of M st p1 in P holds
( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) )
let p1, p2 be Point of M; ::_thesis: ( p1 in P implies ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) )
 dist p2 is continuous by Th16;
then  [#] ((dist p2) .: P) is real-bounded by A1, Th8, Th11;
then A2: ( [#] ((dist p2) .: P) is bounded_above & [#] ((dist p2) .: P) is bounded_below ) by XXREAL_2:def_11;
assume A3: p1 in P ; ::_thesis: ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) )
 ( dist (p1,p2) = (dist p2) . p1 & dom (dist p2) = the carrier of (TopSpaceMetr M) ) by Def4, FUNCT_2:def_1;
then  dist (p1,p2) in [#] ((dist p2) .: P) by A3, FUNCT_1:def_6;
hence  ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) by A2, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum
end;

theorem Th20: :: WEIERSTR:20
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2)
proof
let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2)
let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) )
assume that
A1: P <> {} and
A2: P is compact ; ::_thesis: for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2)
let p1, p2 be Point of M; ::_thesis: abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2)
consider x1 being Point of (TopSpaceMetr M) such that
A3: x1 in P and
A4: (dist p1) . x1 = upper_bound ((dist p1) .: P) by A1, A2, Th14, Th16;
A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider x1 = x1 as Point of M ;
consider x2 being Point of (TopSpaceMetr M) such that
A6: x2 in P and
A7: (dist p2) . x2 = upper_bound ((dist p2) .: P) by A1, A2, Th14, Th16;
reconsider x2 = x2 as Point of M by A5;
A8: dist (x2,p2) = upper_bound ((dist p2) .: P) by A7, Def4;
 (dist p1) . x1 = dist (x1,p1) by Def4;
then  ( dist (x2,p2) <= (dist (x2,p1)) + (dist (p1,p2)) & dist (x2,p1) <= dist (x1,p1) ) by A2, A4, A6, Th19, METRIC_1:4;
then  (dist (x2,p2)) - (dist (x1,p1)) <= ((dist (x2,p1)) + (dist (p1,p2))) - (dist (x2,p1)) by XREAL_1:13;
then A9: - (dist (p1,p2)) <= - ((dist (x2,p2)) - (dist (x1,p1))) by XREAL_1:24;
 (dist p2) . x2 = dist (x2,p2) by Def4;
then  ( dist (x1,p1) <= (dist (x1,p2)) + (dist (p2,p1)) & dist (x1,p2) <= dist (x2,p2) ) by A2, A3, A7, Th19, METRIC_1:4;
then A10: (dist (x1,p1)) - (dist (x2,p2)) <= ((dist (x1,p2)) + (dist (p1,p2))) - (dist (x1,p2)) by XREAL_1:13;
 dist (x1,p1) = upper_bound ((dist p1) .: P) by A4, Def4;
hence  abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) by A8, A10, A9, ABSVALUE:5; ::_thesis: verum
end;

theorem :: WEIERSTR:21
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
proof
let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
abs (x1 - x2) <= dist (p1,p2) )
assume A1: ( P <> {} & P is compact ) ; ::_thesis: for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
let p1, p2 be Point of M; ::_thesis: for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
let x1, x2 be Real; ::_thesis: ( x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 implies abs (x1 - x2) <= dist (p1,p2) )
assume A2: ( x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 ) ; ::_thesis: abs (x1 - x2) <= dist (p1,p2)
 ( (dist_max P) . p1 = upper_bound ((dist p1) .: P) & (dist_max P) . p2 = upper_bound ((dist p2) .: P) ) by Def5;
hence  abs (x1 - x2) <= dist (p1,p2) by A1, A2, Th20; ::_thesis: verum
end;

theorem Th22: :: WEIERSTR:22
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2)
proof
let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2)
let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) )
assume that
A1: P <> {} and
A2: P is compact ; ::_thesis: for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2)
let p1, p2 be Point of M; ::_thesis: abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2)
consider x1 being Point of (TopSpaceMetr M) such that
A3: x1 in P and
A4: (dist p1) . x1 = lower_bound ((dist p1) .: P) by A1, A2, Th15, Th16;
A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider x1 = x1 as Point of M ;
consider x2 being Point of (TopSpaceMetr M) such that
A6: x2 in P and
A7: (dist p2) . x2 = lower_bound ((dist p2) .: P) by A1, A2, Th15, Th16;
reconsider x2 = x2 as Point of M by A5;
A8: dist (x2,p2) = lower_bound ((dist p2) .: P) by A7, Def4;
 (dist p2) . x2 = dist (x2,p2) by Def4;
then  ( dist (x1,p2) <= (dist (x1,p1)) + (dist (p1,p2)) & dist (x2,p2) <= dist (x1,p2) ) by A2, A3, A7, Th19, METRIC_1:4;
then  dist (x2,p2) <= (dist (x1,p1)) + (dist (p1,p2)) by XXREAL_0:2;
then  (dist (x2,p2)) - (dist (x1,p1)) <= dist (p1,p2) by XREAL_1:20;
then A9: - (dist (p1,p2)) <= - ((dist (x2,p2)) - (dist (x1,p1))) by XREAL_1:24;
 (dist p1) . x1 = dist (x1,p1) by Def4;
then  ( dist (x2,p1) <= (dist (x2,p2)) + (dist (p2,p1)) & dist (x1,p1) <= dist (x2,p1) ) by A2, A4, A6, Th19, METRIC_1:4;
then  dist (x1,p1) <= (dist (x2,p2)) + (dist (p1,p2)) by XXREAL_0:2;
then A10: (dist (x1,p1)) - (dist (x2,p2)) <= dist (p1,p2) by XREAL_1:20;
 dist (x1,p1) = lower_bound ((dist p1) .: P) by A4, Def4;
hence  abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) by A8, A10, A9, ABSVALUE:5; ::_thesis: verum
end;

theorem :: WEIERSTR:23
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
proof
let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist (p1,p2) )
assume A1: ( P <> {} & P is compact ) ; ::_thesis: for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
let p1, p2 be Point of M; ::_thesis: for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
let x1, x2 be Real; ::_thesis: ( x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 implies abs (x1 - x2) <= dist (p1,p2) )
assume A2: ( x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 ) ; ::_thesis: abs (x1 - x2) <= dist (p1,p2)
 ( (dist_min P) . p1 = lower_bound ((dist p1) .: P) & (dist_min P) . p2 = lower_bound ((dist p2) .: P) ) by Def6;
hence  abs (x1 - x2) <= dist (p1,p2) by A1, A2, Th22; ::_thesis: verum
end;

Lm2:  [#] R^1 <> {}
;

theorem Th24: :: WEIERSTR:24
for M being non empty MetrSpace
for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_max X is continuous
proof
let M be non empty MetrSpace; ::_thesis: for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_max X is continuous
let X be Subset of (TopSpaceMetr M); ::_thesis: ( X <> {} & X is compact implies dist_max X is continuous )
assume A1: ( X <> {} & X is compact ) ; ::_thesis: dist_max X is continuous
 for P being Subset of R^1 st P is open holds
(dist_max X) " P is open
proof
let P be Subset of R^1; ::_thesis: ( P is open implies (dist_max X) " P is open )
assume A2: P is open ; ::_thesis: (dist_max X) " P is open
 for p being Point of M st p in (dist_max X) " P holds
ex r being real number st
( r > 0 & Ball (p,r) c= (dist_max X) " P )
proof
let p be Point of M; ::_thesis: ( p in (dist_max X) " P implies ex r being real number st
( r > 0 & Ball (p,r) c= (dist_max X) " P ) )
consider y being Point of RealSpace such that
A3: y = upper_bound ((dist p) .: X) by METRIC_1:def_13;
assume  p in (dist_max X) " P ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (dist_max X) " P )
then A4: (dist_max X) . p in P by FUNCT_1:def_7;
reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6;
 y in P by A4, A3, Def5;
then consider r being real number  such that
A5: r > 0 and
A6: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def_6;
reconsider r = r as Real by XREAL_0:def_1;
take  r ; ::_thesis: ( r > 0 & Ball (p,r) c= (dist_max X) " P )
 Ball (p,r) c= (dist_max X) " P
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball (p,r) or z in (dist_max X) " P )
assume A7: z in Ball (p,r) ; ::_thesis: z in (dist_max X) " P
then reconsider z = z as Point of M ;
consider q being Point of RealSpace such that
A8: q = upper_bound ((dist z) .: X) by METRIC_1:def_13;
 dist (p,z) < r by A7, METRIC_1:11;
then  (abs ((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X)))) + (dist (p,z)) < r + (dist (p,z)) by A1, Th20, XREAL_1:8;
then  abs ((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X))) < r by XREAL_1:6;
then  dist (y,q) < r by A3, A8, TOPMETR:11;
then A9: q in Ball (y,r) by METRIC_1:11;
 dom (dist_max X) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then A10: dom (dist_max X) = the carrier of M by TOPMETR:12;
 q = (dist_max X) . z by A8, Def5;
hence  z in (dist_max X) " P by A6, A9, A10, FUNCT_1:def_7; ::_thesis: verum
end;
hence  ( r > 0 & Ball (p,r) c= (dist_max X) " P ) by A5; ::_thesis: verum
end;
hence  (dist_max X) " P is open by TOPMETR:15; ::_thesis: verum
end;
hence  dist_max X is continuous by Lm2, TOPS_2:43; ::_thesis: verum
end;

theorem :: WEIERSTR:25
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in Q & (dist_max P) . x1 = upper_bound ((dist_max P) .: Q) ) by Th14, Th24;

theorem :: WEIERSTR:26
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x2 being Point of (TopSpaceMetr M) st
( x2 in Q & (dist_max P) . x2 = lower_bound ((dist_max P) .: Q) ) by Th15, Th24;

theorem Th27: :: WEIERSTR:27
for M being non empty MetrSpace
for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_min X is continuous
proof
let M be non empty MetrSpace; ::_thesis: for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_min X is continuous
let X be Subset of (TopSpaceMetr M); ::_thesis: ( X <> {} & X is compact implies dist_min X is continuous )
assume A1: ( X <> {} & X is compact ) ; ::_thesis: dist_min X is continuous
 for P being Subset of R^1 st P is open holds
(dist_min X) " P is open
proof
let P be Subset of R^1; ::_thesis: ( P is open implies (dist_min X) " P is open )
assume A2: P is open ; ::_thesis: (dist_min X) " P is open
 for p being Point of M st p in (dist_min X) " P holds
ex r being real number st
( r > 0 & Ball (p,r) c= (dist_min X) " P )
proof
let p be Point of M; ::_thesis: ( p in (dist_min X) " P implies ex r being real number st
( r > 0 & Ball (p,r) c= (dist_min X) " P ) )
assume A3: p in (dist_min X) " P ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (dist_min X) " P )
 ex r being Real st
( r > 0 & Ball (p,r) c= (dist_min X) " P )
proof
A4: (dist_min X) . p in P by A3, FUNCT_1:def_7;
reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6;
consider y being Point of RealSpace such that
A5: y = lower_bound ((dist p) .: X) by METRIC_1:def_13;
 y in P by A4, A5, Def6;
then consider r being real number  such that
A6: r > 0 and
A7: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def_6;
reconsider r = r as Real by XREAL_0:def_1;
take  r ; ::_thesis: ( r > 0 & Ball (p,r) c= (dist_min X) " P )
 Ball (p,r) c= (dist_min X) " P
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball (p,r) or z in (dist_min X) " P )
assume A8: z in Ball (p,r) ; ::_thesis: z in (dist_min X) " P
then reconsider z = z as Point of M ;
consider q being Point of RealSpace such that
A9: q = lower_bound ((dist z) .: X) by METRIC_1:def_13;
 dist (p,z) < r by A8, METRIC_1:11;
then  (abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X)))) + (dist (p,z)) < r + (dist (p,z)) by A1, Th22, XREAL_1:8;
then  abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))) < r by XREAL_1:6;
then  dist (y,q) < r by A5, A9, TOPMETR:11;
then A10: q in Ball (y,r) by METRIC_1:11;
 dom (dist_min X) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then A11: dom (dist_min X) = the carrier of M by TOPMETR:12;
 q = (dist_min X) . z by A9, Def6;
hence  z in (dist_min X) " P by A7, A10, A11, FUNCT_1:def_7; ::_thesis: verum
end;
hence  ( r > 0 & Ball (p,r) c= (dist_min X) " P ) by A6; ::_thesis: verum
end;
hence  ex r being real number st
( r > 0 & Ball (p,r) c= (dist_min X) " P ) ; ::_thesis: verum
end;
hence  (dist_min X) " P is open by TOPMETR:15; ::_thesis: verum
end;
hence  dist_min X is continuous by Lm2, TOPS_2:43; ::_thesis: verum
end;

theorem :: WEIERSTR:28
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in Q & (dist_min P) . x1 = upper_bound ((dist_min P) .: Q) ) by Th14, Th27;

theorem :: WEIERSTR:29
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x2 being Point of (TopSpaceMetr M) st
( x2 in Q & (dist_min P) . x2 = lower_bound ((dist_min P) .: Q) ) by Th15, Th27;

definition
let M be non empty MetrSpace;
let P, Q be Subset of (TopSpaceMetr M);
func min_dist_min (P,Q) ->  Real equals :: WEIERSTR:def 7
 lower_bound ((dist_min P) .: Q);
correctness
coherence
lower_bound ((dist_min P) .: Q) is Real;
;
func max_dist_min (P,Q) ->  Real equals :: WEIERSTR:def 8
 upper_bound ((dist_min P) .: Q);
correctness
coherence
upper_bound ((dist_min P) .: Q) is Real;
;
func min_dist_max (P,Q) ->  Real equals :: WEIERSTR:def 9
 lower_bound ((dist_max P) .: Q);
correctness
coherence
lower_bound ((dist_max P) .: Q) is Real;
;
func max_dist_max (P,Q) ->  Real equals :: WEIERSTR:def 10
 upper_bound ((dist_max P) .: Q);
correctness
coherence
upper_bound ((dist_max P) .: Q) is Real;
;
end;

:: deftheorem  defines min_dist_min WEIERSTR:def_7_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds min_dist_min (P,Q) = lower_bound ((dist_min P) .: Q);

:: deftheorem  defines max_dist_min WEIERSTR:def_8_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds max_dist_min (P,Q) = upper_bound ((dist_min P) .: Q);

:: deftheorem  defines min_dist_max WEIERSTR:def_9_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds min_dist_max (P,Q) = lower_bound ((dist_max P) .: Q);

:: deftheorem  defines max_dist_max WEIERSTR:def_10_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds max_dist_max (P,Q) = upper_bound ((dist_max P) .: Q);

theorem :: WEIERSTR:30
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) )
proof
let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) )
let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) )
assume that
A1: ( P <> {} & P is compact ) and
A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) )
consider x2 being Point of (TopSpaceMetr M) such that
A3: x2 in Q and
A4: (dist_min P) . x2 = lower_bound ((dist_min P) .: Q) by A1, A2, Th15, Th27;
A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider x2 = x2 as Point of M ;
consider x1 being Point of (TopSpaceMetr M) such that
A6: x1 in P and
A7: (dist x2) . x1 = lower_bound ((dist x2) .: P) by A1, Th15, Th16;
reconsider x1 = x1 as Point of M by A5;
take  x1 ; ::_thesis: ex x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) )
take  x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) )
dist (x1,x2) = (dist x2) . x1 by Def4
.= lower_bound ((dist_min P) .: Q) by A4, A7, Def6 ;
hence  ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) by A3, A6; ::_thesis: verum
end;

theorem :: WEIERSTR:31
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) )
proof
let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) )
let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) )
assume that
A1: ( P <> {} & P is compact ) and
A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) )
consider x2 being Point of (TopSpaceMetr M) such that
A3: x2 in Q and
A4: (dist_max P) . x2 = lower_bound ((dist_max P) .: Q) by A1, A2, Th15, Th24;
A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider x2 = x2 as Point of M ;
consider x1 being Point of (TopSpaceMetr M) such that
A6: x1 in P and
A7: (dist x2) . x1 = upper_bound ((dist x2) .: P) by A1, Th14, Th16;
reconsider x1 = x1 as Point of M by A5;
take  x1 ; ::_thesis: ex x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) )
take  x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) )
dist (x1,x2) = (dist x2) . x1 by Def4
.= lower_bound ((dist_max P) .: Q) by A4, A7, Def5 ;
hence  ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) by A3, A6; ::_thesis: verum
end;

theorem :: WEIERSTR:32
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
proof
let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) )
assume that
A1: ( P <> {} & P is compact ) and
A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
consider x2 being Point of (TopSpaceMetr M) such that
A3: x2 in Q and
A4: (dist_min P) . x2 = upper_bound ((dist_min P) .: Q) by A1, A2, Th14, Th27;
A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider x2 = x2 as Point of M ;
consider x1 being Point of (TopSpaceMetr M) such that
A6: x1 in P and
A7: (dist x2) . x1 = lower_bound ((dist x2) .: P) by A1, Th15, Th16;
reconsider x1 = x1 as Point of M by A5;
take  x1 ; ::_thesis: ex x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
take  x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
dist (x1,x2) = (dist x2) . x1 by Def4
.= upper_bound ((dist_min P) .: Q) by A4, A7, Def6 ;
hence  ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) by A3, A6; ::_thesis: verum
end;

theorem :: WEIERSTR:33
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
proof
let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) )
assume that
A1: ( P <> {} & P is compact ) and
A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
consider x2 being Point of (TopSpaceMetr M) such that
A3: x2 in Q and
A4: (dist_max P) . x2 = upper_bound ((dist_max P) .: Q) by A1, A2, Th14, Th24;
A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider x2 = x2 as Point of M ;
consider x1 being Point of (TopSpaceMetr M) such that
A6: x1 in P and
A7: (dist x2) . x1 = upper_bound ((dist x2) .: P) by A1, Th14, Th16;
reconsider x1 = x1 as Point of M by A5;
take  x1 ; ::_thesis: ex x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
take  x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
dist (x1,x2) = (dist x2) . x1 by Def4
.= upper_bound ((dist_max P) .: Q) by A4, A7, Def5 ;
hence  ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) by A3, A6; ::_thesis: verum
end;

theorem :: WEIERSTR:34
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
proof
let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact implies for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) )
assume that
A1: P is compact and
A2: Q is compact ; ::_thesis: for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
let x1, x2 be Point of M; ::_thesis: ( x1 in P & x2 in Q implies ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) )
assume that
A3: x1 in P and
A4: x2 in Q ; ::_thesis: ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
 dist_max P is continuous by A1, A3, Th24;
then  [#] ((dist_max P) .: Q) is real-bounded by A2, Th8, Th11;
then A5: [#] ((dist_max P) .: Q) is bounded_above by XXREAL_2:def_11;
 x2 in the carrier of M ;
then  x2 in the carrier of (TopSpaceMetr M) by TOPMETR:12;
then  (dist_min P) . x2 in the carrier of R^1 by FUNCT_2:5;
then consider z being Real such that
A6: z = (dist_min P) . x2 by TOPMETR:17;
 dist_min P is continuous by A1, A3, Th27;
then  [#] ((dist_min P) .: Q) is real-bounded by A2, Th8, Th11;
then A7: [#] ((dist_min P) .: Q) is bounded_below by XXREAL_2:def_11;
 dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  z in [#] ((dist_min P) .: Q) by A4, A6, FUNCT_1:def_6;
then A8: lower_bound ((dist_min P) .: Q) <= z by A7, SEQ_4:def_2;
 x2 in the carrier of M ;
then  x2 in the carrier of (TopSpaceMetr M) by TOPMETR:12;
then  (dist_max P) . x2 in the carrier of R^1 by FUNCT_2:5;
then consider y being Real such that
A9: y = (dist_max P) . x2 by TOPMETR:17;
 dom (dist_max P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  y in [#] ((dist_max P) .: Q) by A4, A9, FUNCT_1:def_6;
then A10: y <= upper_bound ((dist_max P) .: Q) by A5, SEQ_4:def_1;
A11: lower_bound ((dist x2) .: P) = z by A6, Def6;
A12: upper_bound ((dist x2) .: P) = y by A9, Def5;
 ( dist (x1,x2) <= upper_bound ((dist x2) .: P) & lower_bound ((dist x2) .: P) <= dist (x1,x2) ) by A1, A3, Th19;
hence  ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) by A12, A10, A11, A8, XXREAL_0:2; ::_thesis: verum
end;