:: TBSP_1 semantic presentation

begin


theorem Th1: :: TBSP_1:1
for L being Real st 0 < L & L < 1 holds
for n, m being Element of NAT st n <= m holds
L to_power m <= L to_power n
proof
let L be Real; ::_thesis: ( 0 < L & L < 1 implies for n, m being Element of NAT st n <= m holds
L to_power m <= L to_power n )
assume A1: ( 0 < L & L < 1 ) ; ::_thesis: for n, m being Element of NAT st n <= m holds
L to_power m <= L to_power n
let n, m be Element of NAT ; ::_thesis: ( n <= m implies L to_power m <= L to_power n )
assume A2: n <= m ; ::_thesis: L to_power m <= L to_power n
percases ( n < m or n = m ) by A2, XXREAL_0:1;
suppose n < m ; ::_thesis: L to_power m <= L to_power n
hence  L to_power m <= L to_power n by A1, POWER:40; ::_thesis: verum
end;
suppose n = m ; ::_thesis: L to_power m <= L to_power n
hence  L to_power m <= L to_power n ; ::_thesis: verum
end;
end;
end;

theorem Th2: :: TBSP_1:2
for L being Real st 0 < L & L < 1 holds
for k being Element of NAT holds
( L to_power k <= 1 & 0 < L to_power k )
proof
let L be Real; ::_thesis: ( 0 < L & L < 1 implies for k being Element of NAT holds
( L to_power k <= 1 & 0 < L to_power k ) )
assume that
A1: 0 < L and
A2: L < 1 ; ::_thesis: for k being Element of NAT holds
( L to_power k <= 1 & 0 < L to_power k )
defpred S1[ Element of NAT ] means ( L to_power $1 <= 1 & 0 < L to_power $1 );
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume that
A4: L to_power k <= 1 and
A5: 0 < L to_power k ; ::_thesis: S1[k + 1]
A6: L to_power (k + 1) = (L to_power k) * (L to_power 1) by A1, POWER:27
.= (L to_power k) * L by POWER:25 ;
 (L to_power k) * L <= L to_power k by A2, A5, XREAL_1:153;
hence  S1[k + 1] by A1, A4, A5, A6, XREAL_1:129, XXREAL_0:2; ::_thesis: verum
end;
A7: S1[ 0 ] by POWER:24;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A3); ::_thesis: verum
end;

theorem Th3: :: TBSP_1:3
for L being Real st 0 < L & L < 1 holds
for s being Real st 0 < s holds
ex n being Element of NAT st L to_power n < s
proof
let L be Real; ::_thesis: ( 0 < L & L < 1 implies for s being Real st 0 < s holds
ex n being Element of NAT st L to_power n < s )
assume A1: ( 0 < L & L < 1 ) ; ::_thesis: for s being Real st 0 < s holds
ex n being Element of NAT st L to_power n < s
let s be Real; ::_thesis: ( 0 < s implies ex n being Element of NAT st L to_power n < s )
deffunc H1( Element of NAT ) ->  Element of REAL = L to_power ($1 + 1);
consider rseq being Real_Sequence such that
A2: for n being Element of NAT holds rseq . n = H1(n) from SEQ_1:sch_1();
assume A3: 0 < s ; ::_thesis: ex n being Element of NAT st L to_power n < s
 ( rseq is convergent & lim rseq = 0 ) by A1, A2, SERIES_1:1;
then consider n being Element of NAT  such that
A4: for m being Element of NAT st n <= m holds
abs ((rseq . m) - 0) < s by A3, SEQ_2:def_7;
take  n + 1 ; ::_thesis: L to_power (n + 1) < s
A5: 0 < L to_power (n + 1) by A1, Th2;
abs ((rseq . n) - 0) = abs (L to_power (n + 1)) by A2
.= L to_power (n + 1) by A5, ABSVALUE:def_1 ;
hence  L to_power (n + 1) < s by A4; ::_thesis: verum
end;

definition
let N be non empty MetrStruct ;
attrN is totally_bounded  means :Def1: :: TBSP_1:def 1
 for r being Real st r > 0 holds
ex G being Subset-Family of N st
( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds
ex w being Element of N st C = Ball (w,r) ) );
end;

:: deftheorem Def1 defines totally_bounded TBSP_1:def_1_:_
 for N being non empty MetrStruct holds
( N is totally_bounded iff for r being Real st r > 0 holds
ex G being Subset-Family of N st
( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds
ex w being Element of N st C = Ball (w,r) ) ) );

  Lm1:  for N being non empty MetrStruct
for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
proof
let N be non empty MetrStruct ; ::_thesis: for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
let f be Function; ::_thesis: ( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
thus  ( f is sequence of N implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) ) ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) implies f is sequence of N )
proof
assume A1: f is sequence of N ; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) )
hence  dom f = NAT by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds
f . x is Element of N
let x be set ; ::_thesis: ( x in NAT implies f . x is Element of N )
assume  x in NAT ; ::_thesis: f . x is Element of N
then  x in dom f by A1, FUNCT_2:def_1;
then A2: f . x in rng f by FUNCT_1:def_3;
 rng f c= the carrier of N by A1, RELAT_1:def_19;
hence  f . x is Element of N by A2; ::_thesis: verum
end;
assume that
A3: dom f = NAT and
A4: for x being set st x in NAT holds
f . x is Element of N ; ::_thesis: f is sequence of N
now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_
y_in_the_carrier_of_N
let y be set ; ::_thesis: ( y in rng f implies y in the carrier of N )
assume  y in rng f ; ::_thesis: y in the carrier of N
then consider x being set  such that
A5: x in dom f and
A6: y = f . x by FUNCT_1:def_3;
 f . x is Element of N by A3, A4, A5;
hence  y in the carrier of N by A6; ::_thesis: verum
end;
then  rng f c= the carrier of N by TARSKI:def_3;
hence  f is sequence of N by A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;

theorem :: TBSP_1:4
for N being non empty MetrStruct
for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) )
proof
let N be non empty MetrStruct ; ::_thesis: for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) )
let f be Function; ::_thesis: ( f is sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) )
thus  ( f is sequence of N implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) ) ) by Lm1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of N ) implies f is sequence of N )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n is Element of N ; ::_thesis: f is sequence of N
 for x being set st x in NAT holds
f . x is Element of N by A2;
hence  f is sequence of N by A1, Lm1; ::_thesis: verum
end;

definition
let N be non empty MetrStruct ;
let S2 be sequence of N;
attrS2 is convergent  means :Def2: :: TBSP_1:def 2
 ex x being Element of N st
for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S2 . m),x) < r;
end;

:: deftheorem Def2 defines convergent TBSP_1:def_2_:_
 for N being non empty MetrStruct
for S2 being sequence of N holds
( S2 is convergent iff ex x being Element of N st
for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S2 . m),x) < r );

definition
let M be non empty MetrSpace;
let S1 be sequence of M;
assume A1: S1 is convergent ;
func lim S1 ->  Element of M means :: TBSP_1:def 3
 for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S1 . m),it) < r;
existence
 ex b1 being Element of M st
for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S1 . m),b1) < r by A1, Def2;
uniqueness
 for b1, b2 being Element of M st ( for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S1 . m),b1) < r ) & ( for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S1 . m),b2) < r ) holds
b1 = b2
proof
given g1, g2 being Element of M such that A2: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),g1) < r and
A3: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),g2) < r and
A4: g1 <> g2 ; ::_thesis: contradiction
set a = (dist (g1,g2)) / 4;
A5: dist (g1,g2) >= 0 by METRIC_1:5;
A6: dist (g1,g2) <> 0 by A4, METRIC_1:2;
then consider n1 being Element of NAT  such that
A7: for m being Element of NAT st n1 <= m holds
dist ((S1 . m),g1) < (dist (g1,g2)) / 4 by A2, A5, XREAL_1:224;
consider n2 being Element of NAT  such that
A8: for m being Element of NAT st n2 <= m holds
dist ((S1 . m),g2) < (dist (g1,g2)) / 4 by A3, A6, A5, XREAL_1:224;
set k = n1 + n2;
A9: dist ((S1 . (n1 + n2)),g2) < (dist (g1,g2)) / 4 by A8, NAT_1:12;
A10: dist (g1,g2) <= (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) by METRIC_1:4;
 dist ((S1 . (n1 + n2)),g1) < (dist (g1,g2)) / 4 by A7, NAT_1:12;
then  (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) < ((dist (g1,g2)) / 4) + ((dist (g1,g2)) / 4) by A9, XREAL_1:8;
then  dist (g1,g2) < (dist (g1,g2)) / 2 by A10, XXREAL_0:2;
hence  contradiction by A6, A5, XREAL_1:216; ::_thesis: verum
end;
end;

:: deftheorem  defines lim TBSP_1:def_3_:_
 for M being non empty MetrSpace
for S1 being sequence of M st S1 is convergent holds
for b3 being Element of M holds
( b3 = lim S1 iff for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st m >= n holds
dist ((S1 . m),b3) < r );

definition
let N be non empty MetrStruct ;
let S2 be sequence of N;
attrS2 is Cauchy  means :Def4: :: TBSP_1:def 4
 for r being Real st r > 0 holds
ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r;
end;

:: deftheorem Def4 defines Cauchy TBSP_1:def_4_:_
 for N being non empty MetrStruct
for S2 being sequence of N holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r );

definition
let N be non empty MetrStruct ;
attrN is complete  means :Def5: :: TBSP_1:def 5
 for S2 being sequence of N st S2 is Cauchy holds
S2 is convergent ;
end;

:: deftheorem Def5 defines complete TBSP_1:def_5_:_
 for N being non empty MetrStruct holds
( N is complete iff for S2 being sequence of N st S2 is Cauchy holds
S2 is convergent );

definition
let N be non empty MetrStruct ;
let S2 be sequence of N;
let n be Element of NAT ;
:: original: .
redefine funcS2 . n ->  Element of N;
coherence
 S2 . n is Element of N
proof
thus  S2 . n is Element of N ; ::_thesis: verum
end;
end;

theorem Th5: :: TBSP_1:5
for N being non empty MetrStruct
for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds
S2 is Cauchy
proof
let N be non empty MetrStruct ; ::_thesis: for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds
S2 is Cauchy
let S2 be sequence of N; ::_thesis: ( N is triangle & N is symmetric & S2 is convergent implies S2 is Cauchy )
assume that
A1: N is triangle and
A2: N is symmetric ; ::_thesis: ( not S2 is convergent or S2 is Cauchy )
reconsider N = N as non empty symmetric MetrStruct by A2;
assume A3: S2 is convergent ; ::_thesis: S2 is Cauchy
reconsider S2 = S2 as sequence of N ;
consider g being Element of N such that
A4: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S2 . m),g) < r by A3, Def2;
let r be Real; :: according to TBSP_1:def_4 ::_thesis: ( r > 0 implies ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r )
assume  0 < r ; ::_thesis: ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r
then consider n being Element of NAT  such that
A5: for m being Element of NAT st n <= m holds
dist ((S2 . m),g) < r / 2 by A4, XREAL_1:215;
take  n ; ::_thesis: for n, m being Element of NAT st n <= n & n <= m holds
dist ((S2 . n),(S2 . m)) < r
let m, m9 be Element of NAT ; ::_thesis: ( n <= m & n <= m9 implies dist ((S2 . m),(S2 . m9)) < r )
assume that
A6: m >= n and
A7: m9 >= n ; ::_thesis: dist ((S2 . m),(S2 . m9)) < r
A8: dist ((S2 . m9),g) < r / 2 by A5, A7;
 dist ((S2 . m),g) < r / 2 by A5, A6;
then A9: (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) < (r / 2) + (r / 2) by A8, XREAL_1:8;
 dist ((S2 . m),(S2 . m9)) <= (dist ((S2 . m),g)) + (dist (g,(S2 . m9))) by A1, METRIC_1:4;
hence  dist ((S2 . m),(S2 . m9)) < r by A9, XXREAL_0:2; ::_thesis: verum
end;

registration
let M be non empty symmetric triangle MetrStruct ;
cluster Function-like V33( NAT , the carrier of M) convergent  ->  Cauchy for Element of K10(K11(NAT, the carrier of M));
coherence
 for b1 being sequence of M st b1 is convergent holds
b1 is Cauchy by Th5;
end;

theorem Th6: :: TBSP_1:6
for N being non empty symmetric MetrStruct
for S2 being sequence of N holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r )
proof
let N be non empty symmetric MetrStruct ; ::_thesis: for S2 being sequence of N holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r )
let S2 be sequence of N; ::_thesis: ( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r )
thus  ( S2 is Cauchy implies for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r ) ::_thesis: ( ( for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r ) implies S2 is Cauchy )
proof
assume A1: S2 is Cauchy ; ::_thesis: for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r
let r be Real; ::_thesis: ( r > 0 implies ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r )
assume  0 < r ; ::_thesis: ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r
then consider p being Element of NAT  such that
A2: for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r by A1, Def4;
take  p ; ::_thesis: for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r
let n, k be Element of NAT ; ::_thesis: ( p <= n implies dist ((S2 . (n + k)),(S2 . n)) < r )
assume A3: p <= n ; ::_thesis: dist ((S2 . (n + k)),(S2 . n)) < r
 n <= n + k by NAT_1:11;
then  p <= n + k by A3, XXREAL_0:2;
hence  dist ((S2 . (n + k)),(S2 . n)) < r by A2, A3; ::_thesis: verum
end;
assume A4: for r being Real st r > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r ; ::_thesis: S2 is Cauchy
let r be Real; :: according to TBSP_1:def_4 ::_thesis: ( r > 0 implies ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r )
assume  0 < r ; ::_thesis: ex p being Element of NAT st
for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r
then consider p being Element of NAT  such that
A5: for n, k being Element of NAT st p <= n holds
dist ((S2 . (n + k)),(S2 . n)) < r by A4;
take  p ; ::_thesis: for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r
let n, m be Element of NAT ; ::_thesis: ( p <= n & p <= m implies dist ((S2 . n),(S2 . m)) < r )
assume that
A6: p <= n and
A7: p <= m ; ::_thesis: dist ((S2 . n),(S2 . m)) < r
percases ( n <= m or m <= n ) ;
suppose n <= m ; ::_thesis: dist ((S2 . n),(S2 . m)) < r
then consider k being Nat such that
A8: m = n + k by NAT_1:10;
reconsider m9 = m, n9 = n, k = k as Element of NAT by ORDINAL1:def_12;
 m = n + k by A8;
then  dist ((S2 . m9),(S2 . n9)) < r by A5, A6;
hence  dist ((S2 . n),(S2 . m)) < r ; ::_thesis: verum
end;
suppose m <= n ; ::_thesis: dist ((S2 . n),(S2 . m)) < r
then consider k being Nat such that
A9: n = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 n = m + k by A9;
hence  dist ((S2 . n),(S2 . m)) < r by A5, A7; ::_thesis: verum
end;
end;
end;

theorem :: TBSP_1:7
for M being non empty MetrSpace
for f being Contraction of M st M is complete holds
ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )
proof
let M be non empty MetrSpace; ::_thesis: for f being Contraction of M st M is complete holds
ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )
let f be Contraction of M; ::_thesis: ( M is complete implies ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) )
consider L being Real such that
A1: 0 < L and
A2: L < 1 and
A3: for x, y being Point of M holds dist ((f . x),(f . y)) <= L * (dist (x,y)) by ALI2:def_1;
A4: 1 - L > 0 by A2, XREAL_1:50;
 ex S1 being sequence of M st
for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n)
proof
set z = the Element of M;
deffunc H1( Nat, Element of M) ->  Element of the carrier of M = f . $2;
 ex h being Function of NAT, the carrier of M st
( h . 0 = the Element of M & ( for n being Nat holds h . (n + 1) = H1(n,h . n) ) ) from NAT_1:sch_12();
then consider h being Function of NAT, the carrier of M such that
 h . 0 = the Element of M and
A5: for n being Nat holds h . (n + 1) = f . (h . n) ;
take  h ; ::_thesis: for n being Element of NAT holds h . (n + 1) = f . (h . n)
let n be Element of NAT ; ::_thesis: h . (n + 1) = f . (h . n)
thus  h . (n + 1) = f . (h . n) by A5; ::_thesis: verum
end;
then consider S1 being sequence of M such that
A6: for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n) ;
set r = dist ((S1 . 1),(S1 . 0));
A7: 0 <= dist ((S1 . 1),(S1 . 0)) by METRIC_1:5;
A8: 1 - L <> 0 by A2;
assume A9: M is complete ; ::_thesis: ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )
now__::_thesis:_ex_c_being_Element_of_M_st_
(_f_._c_=_c_&_(_for_y_being_Element_of_M_st_f_._y_=_y_holds_
y_=_c_)_)
percases ( 0 = dist ((S1 . 1),(S1 . 0)) or 0 <> dist ((S1 . 1),(S1 . 0)) ) ;
supposeA10: 0 = dist ((S1 . 1),(S1 . 0)) ; ::_thesis: ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )
A11: f . (S1 . 0) = S1 . (0 + 1) by A6
.= S1 . 0 by A10, METRIC_1:2 ;
 for y being Element of M st f . y = y holds
y = S1 . 0
proof
let y be Element of M; ::_thesis: ( f . y = y implies y = S1 . 0 )
assume A12: f . y = y ; ::_thesis: y = S1 . 0
A13: dist (y,(S1 . 0)) >= 0 by METRIC_1:5;
assume  y <> S1 . 0 ; ::_thesis: contradiction
then  dist (y,(S1 . 0)) <> 0 by METRIC_1:2;
then  L * (dist (y,(S1 . 0))) < dist (y,(S1 . 0)) by A2, A13, XREAL_1:157;
hence  contradiction by A3, A11, A12; ::_thesis: verum
end;
hence  ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) by A11; ::_thesis: verum
end;
supposeA14: 0 <> dist ((S1 . 1),(S1 . 0)) ; ::_thesis: ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )
A15: for n being Element of NAT holds dist ((S1 . (n + 1)),(S1 . n)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power n)
proof
defpred S1[ Element of NAT ] means  dist ((S1 . ($1 + 1)),(S1 . $1)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power $1);
A16: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  dist ((S1 . (k + 1)),(S1 . k)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power k) ; ::_thesis: S1[k + 1]
then A17: L * (dist ((S1 . (k + 1)),(S1 . k))) <= L * ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) by A1, XREAL_1:64;
dist ((S1 . ((k + 1) + 1)),(S1 . (k + 1))) = dist ((f . (S1 . (k + 1))),(S1 . (k + 1))) by A6
.= dist ((f . (S1 . (k + 1))),(f . (S1 . k))) by A6 ;
then A18: dist ((S1 . ((k + 1) + 1)),(S1 . (k + 1))) <= L * (dist ((S1 . (k + 1)),(S1 . k))) by A3;
L * ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) = (dist ((S1 . 1),(S1 . 0))) * (L * (L to_power k))
.= (dist ((S1 . 1),(S1 . 0))) * ((L to_power k) * (L to_power 1)) by POWER:25
.= (dist ((S1 . 1),(S1 . 0))) * (L to_power (k + 1)) by A1, POWER:27 ;
hence  S1[k + 1] by A18, A17, XXREAL_0:2; ::_thesis: verum
end;
dist ((S1 . (0 + 1)),(S1 . 0)) = (dist ((S1 . 1),(S1 . 0))) * 1
.= (dist ((S1 . 1),(S1 . 0))) * (L to_power 0) by POWER:24 ;
then A19: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A19, A16); ::_thesis: verum
end;
A20: for k being Element of NAT holds dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L))
proof
defpred S1[ Element of NAT ] means  dist ((S1 . $1),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power $1)) / (1 - L));
A21: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A22: dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) ; ::_thesis: S1[k + 1]
 dist ((S1 . (k + 1)),(S1 . k)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power k) by A15;
then A23: ( dist ((S1 . (k + 1)),(S1 . 0)) <= (dist ((S1 . (k + 1)),(S1 . k))) + (dist ((S1 . k),(S1 . 0))) & (dist ((S1 . (k + 1)),(S1 . k))) + (dist ((S1 . k),(S1 . 0))) <= ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) + ((dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L))) ) by A22, METRIC_1:4, XREAL_1:7;
((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) + ((dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L))) = (dist ((S1 . 1),(S1 . 0))) * ((L to_power k) + ((1 - (L to_power k)) / (1 - L)))
.= (dist ((S1 . 1),(S1 . 0))) * ((((L to_power k) / (1 - L)) * (1 - L)) + ((1 - (L to_power k)) / (1 - L))) by A8, XCMPLX_1:87
.= (dist ((S1 . 1),(S1 . 0))) * ((((1 - L) * (L to_power k)) / (1 - L)) + ((1 - (L to_power k)) / (1 - L))) by XCMPLX_1:74
.= (dist ((S1 . 1),(S1 . 0))) * ((((1 * (L to_power k)) - (L * (L to_power k))) + (1 - (L to_power k))) / (1 - L)) by XCMPLX_1:62
.= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L * (L to_power k))) / (1 - L))
.= (dist ((S1 . 1),(S1 . 0))) * ((1 - ((L to_power k) * (L to_power 1))) / (1 - L)) by POWER:25
.= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power (k + 1))) / (1 - L)) by A1, POWER:27 ;
hence  S1[k + 1] by A23, XXREAL_0:2; ::_thesis: verum
end;
(dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power 0)) / (1 - L)) = (dist ((S1 . 1),(S1 . 0))) * ((1 - 1) / (1 - L)) by POWER:24
.= 0 ;
then A24: S1[ 0 ] by METRIC_1:1;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A24, A21); ::_thesis: verum
end;
A25: for k being Element of NAT holds dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) / (1 - L)
proof
let k be Element of NAT ; ::_thesis: dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) / (1 - L)
 0 < L to_power k by A1, A2, Th2;
then  1 - (L to_power k) <= 1 by XREAL_1:44;
then  (1 - (L to_power k)) / (1 - L) <= 1 / (1 - L) by A4, XREAL_1:72;
then A26: (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) <= (dist ((S1 . 1),(S1 . 0))) * (1 / (1 - L)) by A7, XREAL_1:64;
 dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) by A20;
then  dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * (1 / (1 - L)) by A26, XXREAL_0:2;
hence  dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) / (1 - L) by XCMPLX_1:99; ::_thesis: verum
end;
A27: for n, k being Element of NAT holds dist ((S1 . (n + k)),(S1 . n)) <= (L to_power n) * (dist ((S1 . k),(S1 . 0)))
proof
defpred S1[ Element of NAT ] means  for k being Element of NAT holds dist ((S1 . ($1 + k)),(S1 . $1)) <= (L to_power $1) * (dist ((S1 . k),(S1 . 0)));
A28: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A29: for k being Element of NAT holds dist ((S1 . (n + k)),(S1 . n)) <= (L to_power n) * (dist ((S1 . k),(S1 . 0))) ; ::_thesis: S1[n + 1]
let k be Element of NAT ; ::_thesis: dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) <= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0)))
A30: L * ((L to_power n) * (dist ((S1 . k),(S1 . 0)))) = (L * (L to_power n)) * (dist ((S1 . k),(S1 . 0)))
.= ((L to_power n) * (L to_power 1)) * (dist ((S1 . k),(S1 . 0))) by POWER:25
.= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0))) by A1, POWER:27 ;
dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) = dist ((S1 . ((n + k) + 1)),(S1 . (n + 1)))
.= dist ((f . (S1 . (n + k))),(S1 . (n + 1))) by A6
.= dist ((f . (S1 . (n + k))),(f . (S1 . n))) by A6 ;
then A31: dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) <= L * (dist ((S1 . (n + k)),(S1 . n))) by A3;
 L * (dist ((S1 . (n + k)),(S1 . n))) <= L * ((L to_power n) * (dist ((S1 . k),(S1 . 0)))) by A1, A29, XREAL_1:64;
hence  dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) <= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0))) by A31, A30, XXREAL_0:2; ::_thesis: verum
end;
A32: S1[ 0 ]
proof
let n be Element of NAT ; ::_thesis: dist ((S1 . (0 + n)),(S1 . 0)) <= (L to_power 0) * (dist ((S1 . n),(S1 . 0)))
(L to_power 0) * (dist ((S1 . n),(S1 . 0))) = 1 * (dist ((S1 . n),(S1 . 0))) by POWER:24
.= dist ((S1 . n),(S1 . 0)) ;
hence  dist ((S1 . (0 + n)),(S1 . 0)) <= (L to_power 0) * (dist ((S1 . n),(S1 . 0))) ; ::_thesis: verum
end;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A32, A28); ::_thesis: verum
end;
A33: for n, k being Element of NAT holds dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n)
proof
let n, k be Element of NAT ; ::_thesis: dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n)
 0 <= L to_power n by A1, A2, Th2;
then A34: (L to_power n) * (dist ((S1 . k),(S1 . 0))) <= (L to_power n) * ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) by A25, XREAL_1:64;
 dist ((S1 . (n + k)),(S1 . n)) <= (L to_power n) * (dist ((S1 . k),(S1 . 0))) by A27;
hence  dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) by A34, XXREAL_0:2; ::_thesis: verum
end;
 for s being Real st s > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S1 . (n + k)),(S1 . n)) < s
proof
A35: (1 - L) / (dist ((S1 . 1),(S1 . 0))) > 0 by A4, A7, A14, XREAL_1:139;
let s be Real; ::_thesis: ( s > 0 implies ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S1 . (n + k)),(S1 . n)) < s )
assume  s > 0 ; ::_thesis: ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist ((S1 . (n + k)),(S1 . n)) < s
then  ((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s > 0 by A35, XREAL_1:129;
then consider p being Element of NAT  such that
A36: L to_power p < ((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s by A1, A2, Th3;
take  p ; ::_thesis: for n, k being Element of NAT st p <= n holds
dist ((S1 . (n + k)),(S1 . n)) < s
let n, k be Element of NAT ; ::_thesis: ( p <= n implies dist ((S1 . (n + k)),(S1 . n)) < s )
assume  p <= n ; ::_thesis: dist ((S1 . (n + k)),(S1 . n)) < s
then  L to_power n <= L to_power p by A1, A2, Th1;
then A37: L to_power n < ((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s by A36, XXREAL_0:2;
 (dist ((S1 . 1),(S1 . 0))) / (1 - L) > 0 by A4, A7, A14, XREAL_1:139;
then A38: ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) < ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s) by A37, XREAL_1:68;
A39: dist ((S1 . (n + k)),(S1 . n)) <= ((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (L to_power n) by A33;
((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * (((1 - L) / (dist ((S1 . 1),(S1 . 0)))) * s) = (((dist ((S1 . 1),(S1 . 0))) / (1 - L)) * ((1 - L) / (dist ((S1 . 1),(S1 . 0))))) * s
.= (((dist ((S1 . 1),(S1 . 0))) * (1 - L)) / ((dist ((S1 . 1),(S1 . 0))) * (1 - L))) * s by XCMPLX_1:76
.= 1 * s by A8, A14, XCMPLX_1:6, XCMPLX_1:60
.= s ;
hence  dist ((S1 . (n + k)),(S1 . n)) < s by A38, A39, XXREAL_0:2; ::_thesis: verum
end;
then  S1 is Cauchy by Th6;
then  S1 is convergent by A9, Def5;
then consider x being Element of M such that
A40: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S1 . m),x) < r by Def2;
A41: f . x = x
proof
set a = (dist (x,(f . x))) / 4;
assume  x <> f . x ; ::_thesis: contradiction
then A42: dist (x,(f . x)) <> 0 by METRIC_1:2;
A43: dist (x,(f . x)) >= 0 by METRIC_1:5;
then consider n being Element of NAT  such that
A44: for m being Element of NAT st n <= m holds
dist ((S1 . m),x) < (dist (x,(f . x))) / 4 by A40, A42, XREAL_1:224;
 dist ((S1 . (n + 1)),(f . x)) = dist ((f . (S1 . n)),(f . x)) by A6;
then A45: dist ((S1 . (n + 1)),(f . x)) <= L * (dist ((S1 . n),x)) by A3;
A46: dist ((S1 . n),x) < (dist (x,(f . x))) / 4 by A44;
 L * (dist ((S1 . n),x)) <= dist ((S1 . n),x) by A2, METRIC_1:5, XREAL_1:153;
then  dist ((S1 . (n + 1)),(f . x)) <= dist ((S1 . n),x) by A45, XXREAL_0:2;
then A47: dist ((S1 . (n + 1)),(f . x)) < (dist (x,(f . x))) / 4 by A46, XXREAL_0:2;
A48: ( dist (x,(f . x)) <= (dist (x,(S1 . (n + 1)))) + (dist ((S1 . (n + 1)),(f . x))) & (dist (x,(f . x))) / 2 < dist (x,(f . x)) ) by A42, A43, METRIC_1:4, XREAL_1:216;
 dist (x,(S1 . (n + 1))) < (dist (x,(f . x))) / 4 by A44, NAT_1:11;
then  (dist (x,(S1 . (n + 1)))) + (dist ((S1 . (n + 1)),(f . x))) < ((dist (x,(f . x))) / 4) + ((dist (x,(f . x))) / 4) by A47, XREAL_1:8;
hence  contradiction by A48, XXREAL_0:2; ::_thesis: verum
end;
 for y being Element of M st f . y = y holds
y = x
proof
let y be Element of M; ::_thesis: ( f . y = y implies y = x )
assume A49: f . y = y ; ::_thesis: y = x
A50: dist (y,x) >= 0 by METRIC_1:5;
assume  y <> x ; ::_thesis: contradiction
then  dist (y,x) <> 0 by METRIC_1:2;
then  L * (dist (y,x)) < dist (y,x) by A2, A50, XREAL_1:157;
hence  contradiction by A3, A41, A49; ::_thesis: verum
end;
hence  ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) by A41; ::_thesis: verum
end;
end;
end;
hence  ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) ; ::_thesis: verum
end;

theorem :: TBSP_1:8
for T being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr T is compact holds
T is complete
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: ( TopSpaceMetr T is compact implies T is complete )
set TM = TopSpaceMetr T;
A1: TopSpaceMetr T = TopStruct(# the carrier of T,(Family_open_set T) #) by PCOMPS_1:def_5;
assume A2: TopSpaceMetr T is compact ; ::_thesis: T is complete
let S2 be sequence of T; :: according to TBSP_1:def_5 ::_thesis: ( S2 is Cauchy implies S2 is convergent )
assume A3: S2 is Cauchy ; ::_thesis: S2 is convergent
 S2 is convergent
proof
A4: for p being Element of NAT holds  {  x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n )  }  <> {}
proof
let p be Element of NAT ; ::_thesis:  {  x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n )  }  <> {}
 S2 . p in  {  x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n )  }  ;
hence   {  x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n )  }  <> {} ; ::_thesis: verum
end;
defpred S1[ Subset of (TopSpaceMetr T)] means  ex p being Element of NAT st $1 =  {  x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n )  }  ;
consider F being Subset-Family of (TopSpaceMetr T) such that
A5: for B being Subset of (TopSpaceMetr T) holds
( B in F iff S1[B] ) from SUBSET_1:sch_3();
defpred S2[ Point of T] means  ex n being Element of NAT st
( 0 <= n & $1 = S2 . n );
set B0 =  {  x where x is Point of T : S2[x]  }  ;
A6:  {  x where x is Point of T : S2[x]  }  is Subset of T from DOMAIN_1:sch_7();
then A7:  {  x where x is Point of T : S2[x]  }  in F by A1, A5;
reconsider B0 =  {  x where x is Point of T : S2[x]  }  as Subset of (TopSpaceMetr T) by A1, A6;
reconsider F = F as Subset-Family of (TopSpaceMetr T) ;
set G = clf F;
A8: Cl B0 in clf F by A7, PCOMPS_1:def_2;
A9: clf F is centered
proof
thus  clf F <> {} by A8; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds
( b1 = {} or not b1 c= clf F or not b1 is finite or not meet b1 = {} )
let H be set ; ::_thesis: ( H = {} or not H c= clf F or not H is finite or not meet H = {} )
assume that
A10: H <> {} and
A11: H c= clf F and
A12: H is finite ; ::_thesis: not meet H = {}
A13: H c= bool the carrier of (TopSpaceMetr T) by A11, XBOOLE_1:1;
 H is c=-linear
proof
let B, C be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B in H or not C in H or B,C are_c=-comparable )
assume that
A14: B in H and
A15: C in H ; ::_thesis: B,C are_c=-comparable
reconsider B = B, C = C as Subset of (TopSpaceMetr T) by A13, A14, A15;
consider V being Subset of (TopSpaceMetr T) such that
A16: B = Cl V and
A17: V in F by A11, A14, PCOMPS_1:def_2;
consider p being Element of NAT  such that
A18: V =  {  x where x is Point of T : ex n being Element of NAT st
( p <= n & x = S2 . n )  }  by A5, A17;
consider W being Subset of (TopSpaceMetr T) such that
A19: C = Cl W and
A20: W in F by A11, A15, PCOMPS_1:def_2;
consider q being Element of NAT  such that
A21: W =  {  x where x is Point of T : ex n being Element of NAT st
( q <= n & x = S2 . n )  }  by A5, A20;
now__::_thesis:_(_(_q_<=_p_&_V_c=_W_)_or_(_p_<=_q_&_W_c=_V_)_)
percases ( q <= p or p <= q ) ;
caseA22: q <= p ; ::_thesis: V c= W
thus  V c= W ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in V or y in W )
assume  y in V ; ::_thesis: y in W
then consider x being Point of T such that
A23: y = x and
A24: ex n being Element of NAT st
( p <= n & x = S2 . n ) by A18;
consider n being Element of NAT  such that
A25: p <= n and
A26: x = S2 . n by A24;
 q <= n by A22, A25, XXREAL_0:2;
hence  y in W by A21, A23, A26; ::_thesis: verum
end;
end;
caseA27: p <= q ; ::_thesis: W c= V
thus  W c= V ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in W or y in V )
assume  y in W ; ::_thesis: y in V
then consider x being Point of T such that
A28: y = x and
A29: ex n being Element of NAT st
( q <= n & x = S2 . n ) by A21;
consider n being Element of NAT  such that
A30: q <= n and
A31: x = S2 . n by A29;
 p <= n by A27, A30, XXREAL_0:2;
hence  y in V by A18, A28, A31; ::_thesis: verum
end;
end;
end;
end;
then  ( B c= C or C c= B ) by A16, A19, PRE_TOPC:19;
hence  B,C are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
then consider m being set  such that
A32: m in H and
A33: for C being set st C in H holds
m c= C by A10, A12, FINSET_1:11;
A34: m c= meet H by A10, A33, SETFAM_1:5;
reconsider m = m as Subset of (TopSpaceMetr T) by A13, A32;
consider A being Subset of (TopSpaceMetr T) such that
A35: m = Cl A and
A36: A in F by A11, A32, PCOMPS_1:def_2;
 A <> {} by A5, A4, A36;
then  m <> {} by A35, PRE_TOPC:18, XBOOLE_1:3;
hence  not meet H = {} by A34; ::_thesis: verum
end;
 clf F is closed by PCOMPS_1:11;
then  meet (clf F) <> {} by A2, A9, COMPTS_1:4;
then consider c being Point of (TopSpaceMetr T) such that
A37: c in meet (clf F) by SUBSET_1:4;
reconsider c = c as Point of T by A1;
take  c ; :: according to TBSP_1:def_2 ::_thesis: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S2 . m),c) < r
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S2 . m),c) < r )
assume  0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S2 . m),c) < r
then A38: 0 < r / 2 by XREAL_1:215;
then consider p being Element of NAT  such that
A39: for n, m being Element of NAT st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r / 2 by A3, Def4;
 dist (c,c) < r / 2 by A38, METRIC_1:1;
then A40: c in Ball (c,(r / 2)) by METRIC_1:11;
reconsider Z = Ball (c,(r / 2)) as Subset of (TopSpaceMetr T) by A1;
 Ball (c,(r / 2)) in Family_open_set T by PCOMPS_1:29;
then A41: Z is open by A1, PRE_TOPC:def_2;
defpred S3[ set ] means  ex n being Element of NAT st
( p <= n & $1 = S2 . n );
set B =  {  x where x is Point of T : S3[x]  }  ;
A42:  {  x where x is Point of T : S3[x]  }  is Subset of T from DOMAIN_1:sch_7();
then A43:  {  x where x is Point of T : S3[x]  }  in F by A1, A5;
reconsider B =  {  x where x is Point of T : S3[x]  }  as Subset of (TopSpaceMetr T) by A1, A42;
 Cl B in clf F by A43, PCOMPS_1:def_2;
then  c in Cl B by A37, SETFAM_1:def_1;
then  B meets Z by A40, A41, PRE_TOPC:def_7;
then consider g being set  such that
A44: g in B /\ Z by XBOOLE_0:4;
take  p ; ::_thesis: for m being Element of NAT st p <= m holds
dist ((S2 . m),c) < r
let m be Element of NAT ; ::_thesis: ( p <= m implies dist ((S2 . m),c) < r )
A45: g in B by A44, XBOOLE_0:def_4;
A46: g in Z by A44, XBOOLE_0:def_4;
then reconsider g = g as Point of T ;
consider x being Point of T such that
A47: g = x and
A48: ex n being Element of NAT st
( p <= n & x = S2 . n ) by A45;
consider n being Element of NAT  such that
A49: p <= n and
A50: x = S2 . n by A48;
assume  p <= m ; ::_thesis: dist ((S2 . m),c) < r
then A51: dist ((S2 . m),(S2 . n)) < r / 2 by A39, A49;
 dist ((S2 . n),c) < r / 2 by A46, A47, A50, METRIC_1:11;
then A52: (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) < (r / 2) + (r / 2) by A51, XREAL_1:8;
 dist ((S2 . m),c) <= (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) by METRIC_1:4;
hence  dist ((S2 . m),c) < r by A52, XXREAL_0:2; ::_thesis: verum
end;
hence  S2 is convergent ; ::_thesis: verum
end;

theorem :: TBSP_1:9
for N being non empty MetrStruct st N is Reflexive & N is triangle & TopSpaceMetr N is compact holds
N is totally_bounded
proof
let N be non empty MetrStruct ; ::_thesis: ( N is Reflexive & N is triangle & TopSpaceMetr N is compact implies N is totally_bounded )
assume A1: N is Reflexive ; ::_thesis: ( not N is triangle or not TopSpaceMetr N is compact or N is totally_bounded )
set TM = TopSpaceMetr N;
assume A2: N is triangle ; ::_thesis: ( not TopSpaceMetr N is compact or N is totally_bounded )
assume A3: TopSpaceMetr N is compact ; ::_thesis: N is totally_bounded
let r be Real; :: according to TBSP_1:def_1 ::_thesis: ( r > 0 implies ex G being Subset-Family of N st
( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds
ex w being Element of N st C = Ball (w,r) ) ) )
assume A4: r > 0 ; ::_thesis: ex G being Subset-Family of N st
( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds
ex w being Element of N st C = Ball (w,r) ) )
defpred S1[ Subset of N] means  ex x being Element of N st $1 = Ball (x,r);
consider G being Subset-Family of N such that
A5: for C being Subset of N holds
( C in G iff S1[C] ) from SUBSET_1:sch_3();
A6: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def_5;
then reconsider G = G as Subset-Family of (TopSpaceMetr N) ;
 for x being Element of (TopSpaceMetr N) holds x in union G
proof
let x be Element of (TopSpaceMetr N); ::_thesis: x in union G
reconsider x = x as Element of N by A6;
 dist (x,x) = 0 by A1, METRIC_1:1;
then A7: x in Ball (x,r) by A4, METRIC_1:11;
 Ball (x,r) in G by A5;
hence  x in union G by A7, TARSKI:def_4; ::_thesis: verum
end;
then  [#] (TopSpaceMetr N) = union G by SUBSET_1:28;
then A8: G is Cover of (TopSpaceMetr N) by SETFAM_1:45;
 for C being Subset of (TopSpaceMetr N) st C in G holds
C is open
proof
let C be Subset of (TopSpaceMetr N); ::_thesis: ( C in G implies C is open )
assume A9: C in G ; ::_thesis: C is open
reconsider C = C as Subset of N by A6;
 ex x being Element of N st C = Ball (x,r) by A5, A9;
then  C in the topology of (TopSpaceMetr N) by A2, A6, PCOMPS_1:29;
hence  C is open by PRE_TOPC:def_2; ::_thesis: verum
end;
then  G is open by TOPS_2:def_1;
then consider H being Subset-Family of (TopSpaceMetr N) such that
A10: H c= G and
A11: H is Cover of (TopSpaceMetr N) and
A12: H is finite by A3, A8, COMPTS_1:def_1;
reconsider H = H as Subset-Family of N by A6;
take  H ; ::_thesis: ( H is finite & the carrier of N = union H & ( for C being Subset of N st C in H holds
ex w being Element of N st C = Ball (w,r) ) )
 union H = the carrier of (TopSpaceMetr N) by A11, SETFAM_1:45;
hence  ( H is finite & the carrier of N = union H & ( for C being Subset of N st C in H holds
ex w being Element of N st C = Ball (w,r) ) ) by A6, A5, A10, A12; ::_thesis: verum
end;

definition
let N be non empty MetrStruct ;
attrN is bounded  means :Def6: :: TBSP_1:def 6
 ex r being Real st
( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) );
let C be Subset of N;
attrC is bounded  means :Def7: :: TBSP_1:def 7
 ex r being Real st
( 0 < r & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r ) );
end;

:: deftheorem Def6 defines bounded TBSP_1:def_6_:_
 for N being non empty MetrStruct holds
( N is bounded iff ex r being Real st
( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) ) );

:: deftheorem Def7 defines bounded TBSP_1:def_7_:_
 for N being non empty MetrStruct
for C being Subset of N holds
( C is bounded iff ex r being Real st
( 0 < r & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r ) ) );

registration
let A be non empty set ;
cluster DiscreteSpace A ->  bounded ;
coherence
 DiscreteSpace A is bounded
proof
take  2 ; :: according to TBSP_1:def_6 ::_thesis: ( 0 < 2 & ( for x, y being Point of (DiscreteSpace A) holds dist (x,y) <= 2 ) )
set N = DiscreteSpace A;
thus  0 < 2 ; ::_thesis: for x, y being Point of (DiscreteSpace A) holds dist (x,y) <= 2
let x, y be Point of (DiscreteSpace A); ::_thesis: dist (x,y) <= 2
A1: ( DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #) & dist (x,y) = the distance of (DiscreteSpace A) . (x,y) ) by METRIC_1:def_1, METRIC_1:def_11;
 ( x = y or x <> y ) ;
then  ( dist (x,y) = 0 or dist (x,y) = 1 ) by A1, METRIC_1:def_10;
hence  dist (x,y) <= 2 ; ::_thesis: verum
end;
end;

registration
cluster non empty Reflexive discerning symmetric triangle Discerning bounded for MetrStruct ;
existence
 ex b1 being non empty MetrSpace st b1 is bounded
proof
take  DiscreteSpace {0} ; ::_thesis: DiscreteSpace {0} is bounded
thus  DiscreteSpace {0} is bounded ; ::_thesis: verum
end;
end;

registration
let N be non empty MetrStruct ;
cluster empty  ->  bounded for Element of K10( the carrier of N);
coherence
 for b1 being Subset of N st b1 is empty holds
b1 is bounded
proof
let S be Subset of N; ::_thesis: ( S is empty implies S is bounded )
assume A1: S is empty ; ::_thesis: S is bounded
take  1 ; :: according to TBSP_1:def_7 ::_thesis: ( 0 < 1 & ( for x, y being Point of N st x in S & y in S holds
dist (x,y) <= 1 ) )
thus  ( 0 < 1 & ( for x, y being Point of N st x in S & y in S holds
dist (x,y) <= 1 ) ) by A1; ::_thesis: verum
end;
end;

registration
let N be non empty MetrStruct ;
cluster bounded for Element of K10( the carrier of N);
existence
 ex b1 being Subset of N st b1 is bounded
proof
take  {} N ; ::_thesis: {} N is bounded
thus  {} N is bounded ; ::_thesis: verum
end;
end;

theorem Th10: :: TBSP_1:10
for N being non empty MetrStruct
for C being Subset of N holds
( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded ) )
proof
let N be non empty MetrStruct ; ::_thesis: for C being Subset of N holds
( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded ) )
let C be Subset of N; ::_thesis: ( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded ) )
thus  ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) ::_thesis: ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded )
proof
set w = the Element of C;
assume A1: C <> {} ; ::_thesis: ( not C is bounded or ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) )
then reconsider w = the Element of C as Point of N by TARSKI:def_3;
assume  C is bounded ; ::_thesis: ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )
then consider r being Real such that
A2: 0 < r and
A3: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r by Def7;
take  r ; ::_thesis: ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )
take  w ; ::_thesis: ( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )
thus  0 < r by A2; ::_thesis: ( w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )
thus  w in C by A1; ::_thesis: for z being Point of N st z in C holds
dist (w,z) <= r
let z be Point of N; ::_thesis: ( z in C implies dist (w,z) <= r )
assume  z in C ; ::_thesis: dist (w,z) <= r
hence  dist (w,z) <= r by A3; ::_thesis: verum
end;
assume A4: N is symmetric ; ::_thesis: ( not N is triangle or for r being Real
for w being Element of N holds
( not 0 < r or ex z being Point of N st
( z in C & not dist (w,z) <= r ) ) or C is bounded )
assume A5: N is triangle ; ::_thesis: ( for r being Real
for w being Element of N holds
( not 0 < r or ex z being Point of N st
( z in C & not dist (w,z) <= r ) ) or C is bounded )
given r being Real, w being Element of N such that A6: 0 < r and
A7: for z being Point of N st z in C holds
dist (w,z) <= r ; ::_thesis: C is bounded
set s = r + r;
reconsider N = N as symmetric MetrStruct by A4;
reconsider w = w as Element of N ;
 ex s being Real st
( 0 < s & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) )
proof
take  r + r ; ::_thesis: ( 0 < r + r & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r + r ) )
thus  0 < r + r by A6; ::_thesis: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r + r
let x, y be Point of N; ::_thesis: ( x in C & y in C implies dist (x,y) <= r + r )
assume that
A8: x in C and
A9: y in C ; ::_thesis: dist (x,y) <= r + r
A10: dist (w,x) <= r by A7, A8;
 dist (w,y) <= r by A7, A9;
then A11: (dist (x,w)) + (dist (w,y)) <= r + r by A10, XREAL_1:7;
 dist (x,y) <= (dist (x,w)) + (dist (w,y)) by A5, METRIC_1:4;
hence  dist (x,y) <= r + r by A11, XXREAL_0:2; ::_thesis: verum
end;
hence  C is bounded by Def7; ::_thesis: verum
end;

theorem Th11: :: TBSP_1:11
for N being non empty MetrStruct
for w being Element of N
for r being real number st N is Reflexive & 0 < r holds
w in Ball (w,r)
proof
let N be non empty MetrStruct ; ::_thesis: for w being Element of N
for r being real number st N is Reflexive & 0 < r holds
w in Ball (w,r)
let w be Element of N; ::_thesis: for r being real number st N is Reflexive & 0 < r holds
w in Ball (w,r)
let r be real number ; ::_thesis: ( N is Reflexive & 0 < r implies w in Ball (w,r) )
assume  N is Reflexive ; ::_thesis: ( not 0 < r or w in Ball (w,r) )
then A1: dist (w,w) = 0 by METRIC_1:1;
assume  0 < r ; ::_thesis: w in Ball (w,r)
hence  w in Ball (w,r) by A1, METRIC_1:11; ::_thesis: verum
end;

theorem Th12: :: TBSP_1:12
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being real number st r <= 0 holds
Ball (t1,r) = {}
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T
for r being real number st r <= 0 holds
Ball (t1,r) = {}
let t1 be Element of T; ::_thesis: for r being real number st r <= 0 holds
Ball (t1,r) = {}
let r be real number ; ::_thesis: ( r <= 0 implies Ball (t1,r) = {} )
assume A1: r <= 0 ; ::_thesis: Ball (t1,r) = {}
set c = the Element of Ball (t1,r);
assume A2: Ball (t1,r) <> {} ; ::_thesis: contradiction
then reconsider c = the Element of Ball (t1,r) as Point of T by TARSKI:def_3;
 dist (t1,c) < r by A2, METRIC_1:11;
hence  contradiction by A1, METRIC_1:5; ::_thesis: verum
end;

Lm2:  for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being real number st 0 < r holds
Ball (t1,r) is bounded
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T
for r being real number st 0 < r holds
Ball (t1,r) is bounded
let t1 be Element of T; ::_thesis: for r being real number st 0 < r holds
Ball (t1,r) is bounded
let r be real number ; ::_thesis: ( 0 < r implies Ball (t1,r) is bounded )
assume A1: 0 < r ; ::_thesis: Ball (t1,r) is bounded
set P = Ball (t1,r);
reconsider r = r as Real by XREAL_0:def_1;
 ex r being Real ex t1 being Element of T st
( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
proof
take  r ; ::_thesis: ex t1 being Element of T st
( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
take  t1 ; ::_thesis: ( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
thus  0 < r by A1; ::_thesis: ( t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
thus  t1 in Ball (t1,r) by A1, Th11; ::_thesis: for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r
let z be Point of T; ::_thesis: ( z in Ball (t1,r) implies dist (t1,z) <= r )
assume  z in Ball (t1,r) ; ::_thesis: dist (t1,z) <= r
hence  dist (t1,z) <= r by METRIC_1:11; ::_thesis: verum
end;
hence  Ball (t1,r) is bounded by Th10; ::_thesis: verum
end;

registration
let T be non empty Reflexive symmetric triangle MetrStruct ;
let t1 be Element of T;
let r be real number ;
cluster Ball (t1,r) ->  bounded ;
coherence
 Ball (t1,r) is bounded
proof
percases ( r <= 0 or 0 < r ) ;
suppose r <= 0 ; ::_thesis: Ball (t1,r) is bounded
then  Ball (t1,r) = {} T by Th12;
hence  Ball (t1,r) is bounded ; ::_thesis: verum
end;
suppose 0 < r ; ::_thesis: Ball (t1,r) is bounded
hence  Ball (t1,r) is bounded by Lm2; ::_thesis: verum
end;
end;
end;
end;

theorem Th13: :: TBSP_1:13
for T being non empty Reflexive symmetric triangle MetrStruct
for P, Q being Subset of T st P is bounded & Q is bounded holds
P \/ Q is bounded
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for P, Q being Subset of T st P is bounded & Q is bounded holds
P \/ Q is bounded
let P, Q be Subset of T; ::_thesis: ( P is bounded & Q is bounded implies P \/ Q is bounded )
assume that
A1: P is bounded and
A2: Q is bounded ; ::_thesis: P \/ Q is bounded
percases ( P = {} or P <> {} ) ;
suppose P = {} ; ::_thesis: P \/ Q is bounded
hence  P \/ Q is bounded by A2; ::_thesis: verum
end;
supposeA3: P <> {} ; ::_thesis: P \/ Q is bounded
now__::_thesis:_P_\/_Q_is_bounded
percases ( Q = {} or Q <> {} ) ;
suppose Q = {} ; ::_thesis: P \/ Q is bounded
hence  P \/ Q is bounded by A1; ::_thesis: verum
end;
suppose Q <> {} ; ::_thesis: P \/ Q is bounded
then consider s being Real, d being Element of T such that
A4: 0 < s and
 d in Q and
A5: for z being Point of T st z in Q holds
dist (d,z) <= s by A2, Th10;
consider r being Real, t1 being Element of T such that
A6: 0 < r and
A7: t1 in P and
A8: for z being Point of T st z in P holds
dist (t1,z) <= r by A1, A3, Th10;
set t = (r + s) + (dist (t1,d));
A9: 0 <= dist (t1,d) by METRIC_1:5;
then A10: r < r + ((dist (t1,d)) + s) by A4, XREAL_1:29;
 ex t being Real ex t1 being Element of T st
( 0 < t & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist (t1,z) <= t ) )
proof
take  (r + s) + (dist (t1,d)) ; ::_thesis: ex t1 being Element of T st
( 0 < (r + s) + (dist (t1,d)) & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist (t1,z) <= (r + s) + (dist (t1,d)) ) )
take  t1 ; ::_thesis: ( 0 < (r + s) + (dist (t1,d)) & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist (t1,z) <= (r + s) + (dist (t1,d)) ) )
thus  0 < (r + s) + (dist (t1,d)) by A6, A4, A9; ::_thesis: ( t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist (t1,z) <= (r + s) + (dist (t1,d)) ) )
thus  t1 in P \/ Q by A7, XBOOLE_0:def_3; ::_thesis: for z being Point of T st z in P \/ Q holds
dist (t1,z) <= (r + s) + (dist (t1,d))
let z be Point of T; ::_thesis: ( z in P \/ Q implies dist (t1,z) <= (r + s) + (dist (t1,d)) )
assume  z in P \/ Q ; ::_thesis: dist (t1,z) <= (r + s) + (dist (t1,d))
then A11: ( z in P or z in Q ) by XBOOLE_0:def_3;
now__::_thesis:_dist_(t1,z)_<=_(r_+_s)_+_(dist_(t1,d))
percases ( dist (t1,z) <= r or dist (d,z) <= s ) by A8, A5, A11;
suppose dist (t1,z) <= r ; ::_thesis: dist (t1,z) <= (r + s) + (dist (t1,d))
hence  dist (t1,z) <= (r + s) + (dist (t1,d)) by A10, XXREAL_0:2; ::_thesis: verum
end;
suppose dist (d,z) <= s ; ::_thesis: dist (t1,z) <= (r + s) + (dist (t1,d))
then  ( dist (t1,z) <= (dist (t1,d)) + (dist (d,z)) & (dist (t1,d)) + (dist (d,z)) <= (dist (t1,d)) + s ) by METRIC_1:4, XREAL_1:7;
then A12: dist (t1,z) <= (dist (t1,d)) + s by XXREAL_0:2;
 (dist (t1,d)) + s <= r + ((dist (t1,d)) + s) by A6, XREAL_1:29;
hence  dist (t1,z) <= (r + s) + (dist (t1,d)) by A12, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  dist (t1,z) <= (r + s) + (dist (t1,d)) ; ::_thesis: verum
end;
hence  P \/ Q is bounded by Th10; ::_thesis: verum
end;
end;
end;
hence  P \/ Q is bounded ; ::_thesis: verum
end;
end;
end;

theorem Th14: :: TBSP_1:14
for N being non empty MetrStruct
for C, D being Subset of N st C is bounded & D c= C holds
D is bounded
proof
let N be non empty MetrStruct ; ::_thesis: for C, D being Subset of N st C is bounded & D c= C holds
D is bounded
let C, D be Subset of N; ::_thesis: ( C is bounded & D c= C implies D is bounded )
assume that
A1: C is bounded and
A2: D c= C ; ::_thesis: D is bounded
consider r being Real such that
A3: 0 < r and
A4: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r by A1, Def7;
 ex r being Real st
( 0 < r & ( for x, y being Point of N st x in D & y in D holds
dist (x,y) <= r ) )
proof
take  r ; ::_thesis: ( 0 < r & ( for x, y being Point of N st x in D & y in D holds
dist (x,y) <= r ) )
thus  0 < r by A3; ::_thesis: for x, y being Point of N st x in D & y in D holds
dist (x,y) <= r
let x, y be Point of N; ::_thesis: ( x in D & y in D implies dist (x,y) <= r )
assume  ( x in D & y in D ) ; ::_thesis: dist (x,y) <= r
hence  dist (x,y) <= r by A2, A4; ::_thesis: verum
end;
hence  D is bounded by Def7; ::_thesis: verum
end;

theorem Th15: :: TBSP_1:15
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for P being Subset of T st P = {t1} holds
P is bounded
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T
for P being Subset of T st P = {t1} holds
P is bounded
let t1 be Element of T; ::_thesis: for P being Subset of T st P = {t1} holds
P is bounded
let P be Subset of T; ::_thesis: ( P = {t1} implies P is bounded )
assume A1: P = {t1} ; ::_thesis: P is bounded
 {t1} is Subset of (Ball (t1,1)) by Th11, SUBSET_1:41;
hence  P is bounded by A1, Th14; ::_thesis: verum
end;

theorem Th16: :: TBSP_1:16
for T being non empty Reflexive symmetric triangle MetrStruct
for P being Subset of T st P is finite holds
P is bounded
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for P being Subset of T st P is finite holds
P is bounded
let P be Subset of T; ::_thesis: ( P is finite implies P is bounded )
defpred S1[ set ] means  ex X being Subset of T st
( X = $1 & X is bounded );
 {} T is bounded ;
then A1: S1[ {} ] ;
A2: for x, B being set st x in P & B c= P & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in P & B c= P & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in P and
 B c= P and
A4: S1[B] ; ::_thesis: S1[B \/ {x}]
reconsider x = x as Element of T by A3;
reconsider W = {x} as Subset of T ;
consider X being Subset of T such that
A5: ( X = B & X is bounded ) by A4;
A6: W is bounded by Th15;
 ex Y being Subset of T st
( Y = B \/ {x} & Y is bounded )
proof
take  X \/ W ; ::_thesis: ( X \/ W = B \/ {x} & X \/ W is bounded )
thus  ( X \/ W = B \/ {x} & X \/ W is bounded ) by A5, A6, Th13; ::_thesis: verum
end;
hence  S1[B \/ {x}] ; ::_thesis: verum
end;
assume A7: P is finite ; ::_thesis: P is bounded
 S1[P] from FINSET_1:sch_2(A7, A1, A2);
hence  P is bounded ; ::_thesis: verum
end;

registration
let T be non empty Reflexive symmetric triangle MetrStruct ;
cluster finite  ->  bounded for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is finite holds
b1 is bounded by Th16;
end;

registration
let T be non empty Reflexive symmetric triangle MetrStruct ;
cluster non empty finite for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st
( b1 is finite & not b1 is empty )
proof
take  the non empty finite Subset of T ; ::_thesis: ( the non empty finite Subset of T is finite & not the non empty finite Subset of T is empty )
thus  ( the non empty finite Subset of T is finite & not the non empty finite Subset of T is empty ) ; ::_thesis: verum
end;
end;

theorem Th17: :: TBSP_1:17
for T being non empty Reflexive symmetric triangle MetrStruct
for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds
P is bounded ) holds
union Y is bounded
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds
P is bounded ) holds
union Y is bounded
let Y be Subset-Family of T; ::_thesis: ( Y is finite & ( for P being Subset of T st P in Y holds
P is bounded ) implies union Y is bounded )
assume that
A1: Y is finite and
A2: for P being Subset of T st P in Y holds
P is bounded ; ::_thesis: union Y is bounded
defpred S1[ set ] means  ex X being Subset of T st
( X = union $1 & X is bounded );
A3: for x, B being set st x in Y & B c= Y & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] )
assume that
A4: x in Y and
 B c= Y and
A5: S1[B] ; ::_thesis: S1[B \/ {x}]
consider X being Subset of T such that
A6: ( X = union B & X is bounded ) by A5;
reconsider x = x as Subset of T by A4;
A7: union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ x by ZFMISC_1:25 ;
A8: x is bounded by A2, A4;
 ex Y being Subset of T st
( Y = union (B \/ {x}) & Y is bounded )
proof
take  X \/ x ; ::_thesis: ( X \/ x = union (B \/ {x}) & X \/ x is bounded )
thus  ( X \/ x = union (B \/ {x}) & X \/ x is bounded ) by A6, A7, A8, Th13; ::_thesis: verum
end;
hence  S1[B \/ {x}] ; ::_thesis: verum
end;
A9: S1[ {} ]
proof
set m = {} T;
 {} T = union {} by ZFMISC_1:2;
hence  S1[ {} ] ; ::_thesis: verum
end;
 S1[Y] from FINSET_1:sch_2(A1, A9, A3);
hence  union Y is bounded ; ::_thesis: verum
end;

theorem Th18: :: TBSP_1:18
for N being non empty MetrStruct holds
( N is bounded iff [#] N is bounded )
proof
let N be non empty MetrStruct ; ::_thesis: ( N is bounded iff [#] N is bounded )
thus  ( N is bounded implies [#] N is bounded ) ::_thesis: ( [#] N is bounded implies N is bounded )
proof
assume  N is bounded ; ::_thesis: [#] N is bounded
then consider r being Real such that
A1: 0 < r and
A2: for x, y being Point of N holds dist (x,y) <= r by Def6;
 for x, y being Point of N st x in [#] N & y in [#] N holds
dist (x,y) <= r by A2;
hence  [#] N is bounded by A1, Def7; ::_thesis: verum
end;
assume  [#] N is bounded ; ::_thesis: N is bounded
then consider r being Real such that
A3: 0 < r and
A4: for x, y being Point of N st x in [#] N & y in [#] N holds
dist (x,y) <= r by Def7;
take  r ; :: according to TBSP_1:def_6 ::_thesis: ( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) )
thus  0 < r by A3; ::_thesis: for x, y being Point of N holds dist (x,y) <= r
let x, y be Point of N; ::_thesis: dist (x,y) <= r
thus  dist (x,y) <= r by A4; ::_thesis: verum
end;

registration
let N be non empty bounded MetrStruct ;
cluster [#] N ->  bounded ;
coherence
 [#] N is bounded by Th18;
end;

theorem :: TBSP_1:19
for T being non empty Reflexive symmetric triangle MetrStruct st T is totally_bounded holds
T is bounded
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: ( T is totally_bounded implies T is bounded )
assume  T is totally_bounded ; ::_thesis: T is bounded
then consider Y being Subset-Family of T such that
A1: ( Y is finite & the carrier of T = union Y ) and
A2: for P being Subset of T st P in Y holds
ex x being Element of T st P = Ball (x,1) by Def1;
 for P being Subset of T st P in Y holds
P is bounded
proof
let P be Subset of T; ::_thesis: ( P in Y implies P is bounded )
assume  P in Y ; ::_thesis: P is bounded
then  ex x being Element of T st P = Ball (x,1) by A2;
hence  P is bounded ; ::_thesis: verum
end;
then  [#] T is bounded by A1, Th17;
hence  T is bounded by Th18; ::_thesis: verum
end;

definition
let N be non empty Reflexive MetrStruct ;
let C be Subset of N;
assume A1: C is bounded ;
func diameter C ->  Real means :Def8: :: TBSP_1:def 8
( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= it ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
it <= s ) ) if C <> {}
otherwise it = 0 ;
consistency
 for b1 being Real holds verum ;
existence
 ( ( C <> {} implies ex b1 being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b1 <= s ) ) ) & ( not C <> {} implies ex b1 being Real st b1 = 0 ) )
proof
thus  ( C <> {} implies ex r being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r <= s ) ) ) ::_thesis: ( not C <> {} implies ex b1 being Real st b1 = 0 )
proof
set c = the Element of C;
defpred S1[ Real] means  for x, y being Point of N st x in C & y in C holds
dist (x,y) <= $1;
set I =  {  r where r is Real : S1[r]  }  ;
defpred S2[ set ] means  ex x, y being Point of N st
( x in C & y in C & $1 = dist (x,y) );
set J =  {  r where r is Real : S2[r]  }  ;
A2: for a, b being real number st a in  {  r where r is Real : S2[r]  }  & b in  {  r where r is Real : S1[r]  }  holds
a <= b
proof
let a, b be real number ; ::_thesis: ( a in  {  r where r is Real : S2[r]  }  & b in  {  r where r is Real : S1[r]  }  implies a <= b )
assume  ( a in  {  r where r is Real : S2[r]  }  & b in  {  r where r is Real : S1[r]  }  ) ; ::_thesis: a <= b
then  ( ex t being Real st
( t = a & ex x, y being Point of N st
( x in C & y in C & t = dist (x,y) ) ) & ex t9 being Real st
( t9 = b & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= t9 ) ) ) ;
hence  a <= b ; ::_thesis: verum
end;
A3:  {  r where r is Real : S2[r]  }  is Subset of REAL from DOMAIN_1:sch_7();
assume A4: C <> {} ; ::_thesis: ex r being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r <= s ) )
then reconsider c = the Element of C as Point of N by TARSKI:def_3;
 dist (c,c) = 0 by METRIC_1:1;
then A5: 0 in  {  r where r is Real : S2[r]  }  by A4;
reconsider J =  {  r where r is Real : S2[r]  }  as Subset of REAL by A3;
A6:  {  r where r is Real : S1[r]  }  is Subset of REAL from DOMAIN_1:sch_7();
consider r being Real such that
 0 < r and
A7: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r by A1, Def7;
A8: r in  {  r where r is Real : S1[r]  }  by A7;
reconsider I =  {  r where r is Real : S1[r]  }  as Subset of REAL by A6;
consider d being real number  such that
A9: for a being real number st a in J holds
a <= d and
A10: for b being real number st b in I holds
d <= b by A8, A5, A2, MEMBERED:37;
take  d ; ::_thesis: ( d is Real & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= d ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
d <= s ) )
thus  d is Real by XREAL_0:def_1; ::_thesis: ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= d ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
d <= s ) )
thus  for x, y being Point of N st x in C & y in C holds
dist (x,y) <= d ::_thesis: for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
d <= s
proof
let x, y be Point of N; ::_thesis: ( x in C & y in C implies dist (x,y) <= d )
assume  ( x in C & y in C ) ; ::_thesis: dist (x,y) <= d
then  dist (x,y) in J ;
hence  dist (x,y) <= d by A9; ::_thesis: verum
end;
let s be Real; ::_thesis: ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) implies d <= s )
assume  for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ; ::_thesis: d <= s
then  s in I ;
hence  d <= s by A10; ::_thesis: verum
end;
thus  ( not C <> {} implies ex b1 being Real st b1 = 0 ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real holds
( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b1 <= s ) & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b2 <= s ) implies b1 = b2 ) & ( not C <> {} & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let r1, r2 be Real; ::_thesis: ( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r2 <= s ) implies r1 = r2 ) & ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 ) )
hereby  ::_thesis: ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 )
assume  C <> {} ; ::_thesis: ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r2 <= s ) implies r1 = r2 )
assume  ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r2 <= s ) ) ; ::_thesis: r1 = r2
then  ( r1 <= r2 & r2 <= r1 ) ;
hence  r1 = r2 by XXREAL_0:1; ::_thesis: verum
end;
thus  ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 ) ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines diameter TBSP_1:def_8_:_
 for N being non empty Reflexive MetrStruct
for C being Subset of N st C is bounded holds
for b3 being Real holds
( ( C <> {} implies ( b3 = diameter C iff ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b3 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b3 <= s ) ) ) ) & ( not C <> {} implies ( b3 = diameter C iff b3 = 0 ) ) );

theorem :: TBSP_1:20
for T being non empty Reflexive symmetric triangle MetrStruct
for x being set
for P being Subset of T st P = {x} holds
diameter P = 0
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for x being set
for P being Subset of T st P = {x} holds
diameter P = 0
let x be set ; ::_thesis: for P being Subset of T st P = {x} holds
diameter P = 0
let P be Subset of T; ::_thesis: ( P = {x} implies diameter P = 0 )
assume A1: P = {x} ; ::_thesis: diameter P = 0
then A2: x in P by TARSKI:def_1;
then reconsider t1 = x as Element of T ;
 ( ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= 0 ) & ( for s being Real st ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ) holds
0 <= s ) )
proof
thus  for x, y being Point of T st x in P & y in P holds
dist (x,y) <= 0 ::_thesis: for s being Real st ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ) holds
0 <= s
proof
let x, y be Point of T; ::_thesis: ( x in P & y in P implies dist (x,y) <= 0 )
assume that
A3: x in P and
A4: y in P ; ::_thesis: dist (x,y) <= 0
 x = t1 by A1, A3, TARSKI:def_1;
then  dist (x,y) = dist (t1,t1) by A1, A4, TARSKI:def_1
.= 0 by METRIC_1:1 ;
hence  dist (x,y) <= 0 ; ::_thesis: verum
end;
let s be Real; ::_thesis: ( ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ) implies 0 <= s )
assume  for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ; ::_thesis: 0 <= s
then  dist (t1,t1) <= s by A2;
hence  0 <= s by METRIC_1:1; ::_thesis: verum
end;
hence  diameter P = 0 by A1, Def8; ::_thesis: verum
end;

theorem Th21: :: TBSP_1:21
for R being non empty Reflexive MetrStruct
for S being Subset of R st S is bounded holds
0 <= diameter S
proof
let R be non empty Reflexive MetrStruct ; ::_thesis: for S being Subset of R st S is bounded holds
0 <= diameter S
let S be Subset of R; ::_thesis: ( S is bounded implies 0 <= diameter S )
assume A1: S is bounded ; ::_thesis: 0 <= diameter S
percases ( S = {} or S <> {} ) ;
suppose S = {} ; ::_thesis: 0 <= diameter S
hence  0 <= diameter S by Def8; ::_thesis: verum
end;
supposeA2: S <> {} ; ::_thesis: 0 <= diameter S
set x = the Element of S;
reconsider x = the Element of S as Element of R by A2, TARSKI:def_3;
 dist (x,x) <= diameter S by A1, A2, Def8;
hence  0 <= diameter S by METRIC_1:1; ::_thesis: verum
end;
end;
end;

theorem :: TBSP_1:22
for M being non empty MetrSpace
for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds
ex g being Point of M st A = {g}
proof
let M be non empty MetrSpace; ::_thesis: for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds
ex g being Point of M st A = {g}
let A be Subset of M; ::_thesis: ( A <> {} & A is bounded & diameter A = 0 implies ex g being Point of M st A = {g} )
assume that
A1: A <> {} and
A2: A is bounded ; ::_thesis: ( not diameter A = 0 or ex g being Point of M st A = {g} )
thus  ( diameter A = 0 implies ex g being Point of M st A = {g} ) ::_thesis: verum
proof
set g = the Element of A;
reconsider g = the Element of A as Element of M by A1, TARSKI:def_3;
assume A3: diameter A = 0 ; ::_thesis: ex g being Point of M st A = {g}
reconsider Z = {g} as Subset of M ;
take  g ; ::_thesis: A = {g}
 for x being Element of M holds
( x in A iff x in Z )
proof
let x be Element of M; ::_thesis: ( x in A iff x in Z )
thus  ( x in A implies x in Z ) ::_thesis: ( x in Z implies x in A )
proof
assume  x in A ; ::_thesis: x in Z
then  dist (x,g) <= 0 by A2, A3, Def8;
then  dist (x,g) = 0 by METRIC_1:5;
then  x = g by METRIC_1:2;
hence  x in Z by TARSKI:def_1; ::_thesis: verum
end;
assume A4: x in Z ; ::_thesis: x in A
 g in A by A1;
hence  x in A by A4, TARSKI:def_1; ::_thesis: verum
end;
hence  A = {g} by SUBSET_1:3; ::_thesis: verum
end;
end;

theorem :: TBSP_1:23
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being Real st 0 < r holds
diameter (Ball (t1,r)) <= 2 * r
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for t1 being Element of T
for r being Real st 0 < r holds
diameter (Ball (t1,r)) <= 2 * r
let t1 be Element of T; ::_thesis: for r being Real st 0 < r holds
diameter (Ball (t1,r)) <= 2 * r
let r be Real; ::_thesis: ( 0 < r implies diameter (Ball (t1,r)) <= 2 * r )
A1: for x, y being Point of T st x in Ball (t1,r) & y in Ball (t1,r) holds
dist (x,y) <= 2 * r
proof
let x, y be Point of T; ::_thesis: ( x in Ball (t1,r) & y in Ball (t1,r) implies dist (x,y) <= 2 * r )
assume  ( x in Ball (t1,r) & y in Ball (t1,r) ) ; ::_thesis: dist (x,y) <= 2 * r
then  ( dist (t1,x) < r & dist (t1,y) < r ) by METRIC_1:11;
then A2: (dist (t1,x)) + (dist (t1,y)) < r + r by XREAL_1:8;
 dist (x,y) <= (dist (x,t1)) + (dist (t1,y)) by METRIC_1:4;
hence  dist (x,y) <= 2 * r by A2, XXREAL_0:2; ::_thesis: verum
end;
assume  0 < r ; ::_thesis: diameter (Ball (t1,r)) <= 2 * r
then  t1 in Ball (t1,r) by Th11;
hence  diameter (Ball (t1,r)) <= 2 * r by A1, Def8; ::_thesis: verum
end;

theorem :: TBSP_1:24
for R being non empty Reflexive MetrStruct
for S, V being Subset of R st S is bounded & V c= S holds
diameter V <= diameter S
proof
let R be non empty Reflexive MetrStruct ; ::_thesis: for S, V being Subset of R st S is bounded & V c= S holds
diameter V <= diameter S
let S, V be Subset of R; ::_thesis: ( S is bounded & V c= S implies diameter V <= diameter S )
assume that
A1: S is bounded and
A2: V c= S ; ::_thesis: diameter V <= diameter S
A3: V is bounded by A1, A2, Th14;
percases ( V = {} or V <> {} ) ;
suppose V = {} ; ::_thesis: diameter V <= diameter S
then  diameter V = 0 by Def8;
hence  diameter V <= diameter S by A1, Th21; ::_thesis: verum
end;
supposeA4: V <> {} ; ::_thesis: diameter V <= diameter S
 for x, y being Point of R st x in V & y in V holds
dist (x,y) <= diameter S by A1, A2, Def8;
hence  diameter V <= diameter S by A3, A4, Def8; ::_thesis: verum
end;
end;
end;

theorem :: TBSP_1:25
for T being non empty Reflexive symmetric triangle MetrStruct
for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds
diameter (P \/ Q) <= (diameter P) + (diameter Q)
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds
diameter (P \/ Q) <= (diameter P) + (diameter Q)
let P, Q be Subset of T; ::_thesis: ( P is bounded & Q is bounded & P meets Q implies diameter (P \/ Q) <= (diameter P) + (diameter Q) )
assume that
A1: P is bounded and
A2: Q is bounded and
A3: P /\ Q <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: diameter (P \/ Q) <= (diameter P) + (diameter Q)
set g = the Element of P /\ Q;
A4: the Element of P /\ Q in Q by A3, XBOOLE_0:def_4;
set s = (diameter P) + (diameter Q);
set b = diameter Q;
A5: diameter Q <= (diameter P) + (diameter Q) by A1, Th21, XREAL_1:31;
set a = diameter P;
A6: the Element of P /\ Q in P by A3, XBOOLE_0:def_4;
reconsider g = the Element of P /\ Q as Element of T by A3, TARSKI:def_3;
A7: diameter P <= (diameter P) + (diameter Q) by A2, Th21, XREAL_1:31;
A8: for x, y being Point of T st x in P \/ Q & y in P \/ Q holds
dist (x,y) <= (diameter P) + (diameter Q)
proof
let x, y be Point of T; ::_thesis: ( x in P \/ Q & y in P \/ Q implies dist (x,y) <= (diameter P) + (diameter Q) )
assume that
A9: x in P \/ Q and
A10: y in P \/ Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q)
A11: dist (x,y) <= (dist (x,g)) + (dist (g,y)) by METRIC_1:4;
now__::_thesis:_dist_(x,y)_<=_(diameter_P)_+_(diameter_Q)
percases ( x in P or x in Q ) by A9, XBOOLE_0:def_3;
supposeA12: x in P ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q)
now__::_thesis:_dist_(x,y)_<=_(diameter_P)_+_(diameter_Q)
percases ( y in P or y in Q ) by A10, XBOOLE_0:def_3;
suppose y in P ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q)
then  dist (x,y) <= diameter P by A1, A12, Def8;
hence  dist (x,y) <= (diameter P) + (diameter Q) by A7, XXREAL_0:2; ::_thesis: verum
end;
supposeA13: y in Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q)
A14: dist (x,g) <= diameter P by A1, A6, A12, Def8;
 dist (g,y) <= diameter Q by A2, A4, A13, Def8;
then  (dist (x,g)) + (dist (g,y)) <= (diameter P) + (diameter Q) by A14, XREAL_1:7;
hence  dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  dist (x,y) <= (diameter P) + (diameter Q) ; ::_thesis: verum
end;
supposeA15: x in Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q)
now__::_thesis:_dist_(x,y)_<=_(diameter_P)_+_(diameter_Q)
percases ( y in P or y in Q ) by A10, XBOOLE_0:def_3;
supposeA16: y in P ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q)
A17: dist (x,g) <= diameter Q by A2, A4, A15, Def8;
 dist (g,y) <= diameter P by A1, A6, A16, Def8;
then  (dist (x,g)) + (dist (g,y)) <= (diameter Q) + (diameter P) by A17, XREAL_1:7;
hence  dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; ::_thesis: verum
end;
suppose y in Q ; ::_thesis: dist (x,y) <= (diameter P) + (diameter Q)
then  dist (x,y) <= diameter Q by A2, A15, Def8;
hence  dist (x,y) <= (diameter P) + (diameter Q) by A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  dist (x,y) <= (diameter P) + (diameter Q) ; ::_thesis: verum
end;
end;
end;
hence  dist (x,y) <= (diameter P) + (diameter Q) ; ::_thesis: verum
end;
 ( P <> {} & P \/ Q is bounded ) by A1, A2, A3, Th13;
hence  diameter (P \/ Q) <= (diameter P) + (diameter Q) by A8, Def8; ::_thesis: verum
end;

theorem :: TBSP_1:26
for T being non empty Reflexive symmetric triangle MetrStruct
for S1 being sequence of T st S1 is Cauchy holds
rng S1 is bounded
proof
let T be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for S1 being sequence of T st S1 is Cauchy holds
rng S1 is bounded
let S1 be sequence of T; ::_thesis: ( S1 is Cauchy implies rng S1 is bounded )
set A = rng S1;
assume  S1 is Cauchy ; ::_thesis: rng S1 is bounded
then consider p being Element of NAT  such that
A1: for n, m being Element of NAT st p <= n & p <= m holds
dist ((S1 . n),(S1 . m)) < 1 by Def4;
defpred S1[ set ] means  ex n being Element of NAT st
( p <= n & $1 = S1 . n );
reconsider B =  {  t1 where t1 is Point of T : S1[t1]  }  as Subset of T from DOMAIN_1:sch_7();
defpred S2[ set ] means  ex n being Element of NAT st
( n <= p & $1 = S1 . n );
reconsider C =  {  t1 where t1 is Point of T : S2[t1]  }  as Subset of T from DOMAIN_1:sch_7();
reconsider B = B, C = C as Subset of T ;
A2: C is finite
proof
set K = Seg p;
set J = {0} \/ (Seg p);
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_C_implies_x_in_S1_.:_({0}_\/_(Seg_p))_)_&_(_x_in_S1_.:_({0}_\/_(Seg_p))_implies_x_in_C_)_)
let x be set ; ::_thesis: ( ( x in C implies x in S1 .: ({0} \/ (Seg p)) ) & ( x in S1 .: ({0} \/ (Seg p)) implies x in C ) )
thus  ( x in C implies x in S1 .: ({0} \/ (Seg p)) ) ::_thesis: ( x in S1 .: ({0} \/ (Seg p)) implies x in C )
proof
assume  x in C ; ::_thesis: x in S1 .: ({0} \/ (Seg p))
then consider t1 being Element of T such that
A3: x = t1 and
A4: ex n being Element of NAT st
( n <= p & t1 = S1 . n ) ;
consider n being Element of NAT  such that
A5: n <= p and
A6: t1 = S1 . n by A4;
 n in NAT ;
then A7: n in dom S1 by FUNCT_2:def_1;
now__::_thesis:_x_in_S1_.:_({0}_\/_(Seg_p))
percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose n = 0 ; ::_thesis: x in S1 .: ({0} \/ (Seg p))
then  n in {0} by TARSKI:def_1;
then  n in {0} \/ (Seg p) by XBOOLE_0:def_3;
hence  x in S1 .: ({0} \/ (Seg p)) by A3, A6, A7, FUNCT_1:def_6; ::_thesis: verum
end;
suppose ex m being Nat st n = m + 1 ; ::_thesis: x in S1 .: ({0} \/ (Seg p))
then  1 <= n by NAT_1:11;
then  n in  {  k where k is Element of NAT : ( 1 <= k & k <= p )  }  by A5;
then  n in Seg p by FINSEQ_1:def_1;
then  n in {0} \/ (Seg p) by XBOOLE_0:def_3;
hence  x in S1 .: ({0} \/ (Seg p)) by A3, A6, A7, FUNCT_1:def_6; ::_thesis: verum
end;
end;
end;
hence  x in S1 .: ({0} \/ (Seg p)) ; ::_thesis: verum
end;
assume  x in S1 .: ({0} \/ (Seg p)) ; ::_thesis: x in C
then consider y being set  such that
A8: y in dom S1 and
A9: y in {0} \/ (Seg p) and
A10: x = S1 . y by FUNCT_1:def_6;
reconsider y = y as Element of NAT by A8;
now__::_thesis:_x_in_C
percases ( y in {0} or y in Seg p ) by A9, XBOOLE_0:def_3;
supposeA11: y in {0} ; ::_thesis: x in C
 S1 . y is Element of T ;
then reconsider x9 = x as Element of T by A10;
 y = 0 by A11, TARSKI:def_1;
then  ex n being Element of NAT st
( n <= p & x9 = S1 . n ) by A10;
hence  x in C ; ::_thesis: verum
end;
supposeA12: y in Seg p ; ::_thesis: x in C
 S1 . y is Element of T ;
then reconsider x9 = x as Element of T by A10;
 y in  {  k where k is Element of NAT : ( 1 <= k & k <= p )  }  by A12, FINSEQ_1:def_1;
then  ex k being Element of NAT st
( y = k & 1 <= k & k <= p ) ;
then  ex n being Element of NAT st
( n <= p & x9 = S1 . n ) by A10;
hence  x in C ; ::_thesis: verum
end;
end;
end;
hence  x in C ; ::_thesis: verum
end;
hence  C is finite by TARSKI:1; ::_thesis: verum
end;
A13: rng S1 = B \/ C
proof
thus  rng S1 c= B \/ C :: according to XBOOLE_0:def_10 ::_thesis: B \/ C c= rng S1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng S1 or x in B \/ C )
assume  x in rng S1 ; ::_thesis: x in B \/ C
then consider y being set  such that
A14: y in dom S1 and
A15: x = S1 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A14;
 S1 . y is Element of T ;
then reconsider x9 = x as Element of T by A15;
percases ( y <= p or p <= y ) ;
suppose y <= p ; ::_thesis: x in B \/ C
then  ex n being Element of NAT st
( n <= p & x9 = S1 . n ) by A15;
then  x in C ;
hence  x in B \/ C by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose p <= y ; ::_thesis: x in B \/ C
then  ex n being Element of NAT st
( p <= n & x9 = S1 . n ) by A15;
then  x in B ;
hence  x in B \/ C by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B \/ C or x in rng S1 )
assume A16: x in B \/ C ; ::_thesis: x in rng S1
percases ( x in B or x in C ) by A16, XBOOLE_0:def_3;
suppose x in B ; ::_thesis: x in rng S1
then consider t1 being Element of T such that
A17: x = t1 and
A18: ex n being Element of NAT st
( p <= n & t1 = S1 . n ) ;
consider n being Element of NAT  such that
 p <= n and
A19: t1 = S1 . n by A18;
 n in NAT ;
then  n in dom S1 by FUNCT_2:def_1;
hence  x in rng S1 by A17, A19, FUNCT_1:def_3; ::_thesis: verum
end;
suppose x in C ; ::_thesis: x in rng S1
then consider t1 being Element of T such that
A20: x = t1 and
A21: ex n being Element of NAT st
( n <= p & t1 = S1 . n ) ;
consider n being Element of NAT  such that
 n <= p and
A22: t1 = S1 . n by A21;
 n in NAT ;
then  n in dom S1 by FUNCT_2:def_1;
hence  x in rng S1 by A20, A22, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
 B is bounded
proof
set x = S1 . p;
 ex r being Real ex t1 being Element of T st
( 0 < r & t1 in B & ( for z being Point of T st z in B holds
dist (t1,z) <= r ) )
proof
take  1 ; ::_thesis: ex t1 being Element of T st
( 0 < 1 & t1 in B & ( for z being Point of T st z in B holds
dist (t1,z) <= 1 ) )
take  S1 . p ; ::_thesis: ( 0 < 1 & S1 . p in B & ( for z being Point of T st z in B holds
dist ((S1 . p),z) <= 1 ) )
thus  0 < 1 ; ::_thesis: ( S1 . p in B & ( for z being Point of T st z in B holds
dist ((S1 . p),z) <= 1 ) )
thus  S1 . p in B ; ::_thesis: for z being Point of T st z in B holds
dist ((S1 . p),z) <= 1
let z be Point of T; ::_thesis: ( z in B implies dist ((S1 . p),z) <= 1 )
assume  z in B ; ::_thesis: dist ((S1 . p),z) <= 1
then  ex t1 being Element of T st
( z = t1 & ex n being Element of NAT st
( p <= n & t1 = S1 . n ) ) ;
hence  dist ((S1 . p),z) <= 1 by A1; ::_thesis: verum
end;
hence  B is bounded by Th10; ::_thesis: verum
end;
hence  rng S1 is bounded by A2, A13, Th13; ::_thesis: verum
end;