let Z be non empty MetrSpace; :: thesis:
let H be non empty Subset of Z; :: thesis:
consider D being Subset of (TopSpaceMetr Z) such that
A1: ( D = H & Cl H = Cl D ) by ASCOLI:def 1;
A2: H c= Cl H by A1, PRE_TOPC:18;
A3: the carrier of (Z | H) = H by TOPMETR:def 2;
A4: the carrier of (Z | (Cl H)) = Cl H by TOPMETR:def 2;

hereby :: thesis:

assume A5: Z | H is totally_bounded ; :: thesis:
for r being Real st r > 0 holds
ex L being Subset-Family of (Z | (Cl H)) st
( L is finite & the carrier of (Z | (Cl H)) = union L & ( for C being Subset of (Z | (Cl H)) st C in L holds
ex w being Element of (Z | (Cl H)) st C = Ball (w,r) ) )

let r be Real; :: thesis:
assume A6: r > 0 ; :: thesis:
then consider L0 being Subset-Family of (Z | H) such that
A7: ( L0 is finite & the carrier of (Z | H) = union L0 & ( for C being Subset of (Z | H) st C in L0 holds
ex w being Element of (Z | H) st C = Ball (w,(r / 2)) ) ) by A5;
defpred S₁[ object , object ] means ex w being Point of (Z | H) st
( $2 = w & $1 = Ball (w,(r / 2)) );
A8: for D being object st D in L0 holds
ex w being object st
( w in the carrier of (Z | H) & S₁[D,w] )

proof

let D be object ; :: thesis:
assume A9: D in L0 ; :: thesis:
then reconsider D0 = D as Subset of (Z | H) ;
consider w being Element of (Z | H) such that
A10: D0 = Ball (w,(r / 2)) by A7, A9;
take w ; :: thesis:
thus ( w in the carrier of (Z | H) & S₁[D,w] ) by A10; :: thesis:

end;

consider U0 being Function of L0, the carrier of (Z | H) such that
A11: for D being object st D in L0 holds
S₁[D,U0 . D] from FUNCT_2:sch 1(A8);
A12: for D being object st D in L0 holds
D = Ball ((U0 /. D),(r / 2))

proof

let D be object ; :: thesis:
assume A13: D in L0 ; :: thesis:
then A14: ex x0 being Point of (Z | H) st
( U0 . D = x0 & D = Ball (x0,(r / 2)) ) by A11;
dom U0 = L0 by FUNCT_2:def 1;
hence D = Ball ((U0 /. D),(r / 2)) by A14, A13, PARTFUN1:def 6; :: thesis:

end;

defpred S₂[ object , object ] means ex x being Point of (Z | (Cl H)) st
( $1 = x & $2 = Ball (x,r) );
A15: for w being object st w in the carrier of (Z | H) holds
ex B being object st
( B in bool the carrier of (Z | (Cl H)) & S₂[w,B] )

proof

let w be object ; :: thesis:
assume w in the carrier of (Z | H) ; :: thesis:
then reconsider x = w as Point of (Z | (Cl H)) by A2, A3, TOPMETR:def 2;
Ball (x,r) in bool the carrier of (Z | (Cl H)) ;
hence ex B being object st
( B in bool the carrier of (Z | (Cl H)) & S₂[w,B] ) ; :: thesis:

end;

consider B being Function of the carrier of (Z | H),(bool the carrier of (Z | (Cl H))) such that
A16: for x being object st x in the carrier of (Z | H) holds
S₂[x,B . x] from FUNCT_2:sch 1(A15);
A17: dom U0 = L0 by FUNCT_2:def 1;
reconsider L = B .: (rng U0) as Subset-Family of (Z | (Cl H)) ;
take L ; :: thesis:
thus L is finite by A7; :: thesis:
the carrier of (Z | (Cl H)) c= union L

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A18: z in the carrier of (Z | (Cl H)) ; :: thesis:
then consider seq being sequence of Z such that
A19: ( ( for n being Nat holds seq . n in H ) & seq is convergent & lim seq = z ) by A1, A4, TOPMETR4:5;
seq is_convergent_in_metrspace_to lim seq by A19, METRIC_6:12;
then consider N being Nat such that
A20: for n being Nat st N <= n holds
dist ((seq . n),(lim seq)) < r / 2 by METRIC_6:def 2, A6;
A21: dist ((seq . N),(lim seq)) < r / 2 by A20;
seq . N in H by A19;
then consider D being set such that
A22: ( seq . N in D & D in L0 ) by A7, A3, TARSKI:def 4;
reconsider y0 = seq . N as Point of (Z | H) by A19, A3;
A23: D = Ball ((U0 /. D),(r / 2)) by A12, A22;
y0 in { y where y is Point of (Z | H) : dist ((U0 /. D),y) < r / 2 } by METRIC_1:def 14, A22, A23;
then A24: ex y being Point of (Z | H) st
( y0 = y & dist ((U0 /. D),y) < r / 2 ) ;
reconsider y01 = y0 as Point of Z ;
reconsider u0d1 = U0 /. D as Point of Z by TOPMETR:def 1, TARSKI:def 3;
A25: dist (u0d1,y01) < r / 2 by A24, TOPMETR:def 1;
U0 /. D in H by A3;
then reconsider u0d = U0 /. D as Point of Z ;
A27: dist (u0d,(lim seq)) <= (dist (u0d,(seq . N))) + (dist ((seq . N),(lim seq))) by METRIC_1:4;
(dist (u0d,(seq . N))) + (dist ((seq . N),(lim seq))) < (r / 2) + (r / 2) by XREAL_1:8, A25, A21;
then A28: dist (u0d,(lim seq)) < r by A27, XXREAL_0:2;
reconsider w = U0 /. D as Point of (Z | (Cl H)) by A2, A3, A4;
reconsider v = lim seq as Point of (Z | (Cl H)) by A19, A18;
dist (w,v) < r by A28, TOPMETR:def 1;
then v in { y where y is Point of (Z | (Cl H)) : dist (w,y) < r } ;
then A29: v in Ball (w,r) by METRIC_1:def 14;
A30: ex w being Point of (Z | (Cl H)) st
( U0 /. D = w & B . (U0 /. D) = Ball (w,r) ) by A16;
U0 /. D in rng U0 by PARTFUN2:2, A22, A17;
then Ball (w,r) in L by A30, FUNCT_2:35;
hence z in union L by A19, A29, TARSKI:def 4; :: thesis:

end;

hence the carrier of (Z | (Cl H)) = union L ; :: thesis:
thus for C being Subset of (Z | (Cl H)) st C in L holds
ex w being Element of (Z | (Cl H)) st C = Ball (w,r) :: thesis:

proof

let C be Subset of (Z | (Cl H)); :: thesis:
assume C in L ; :: thesis:
then consider x being Element of (Z | H) such that
A31: ( x in rng U0 & C = B . x ) by FUNCT_2:65;
ex w being Point of (Z | (Cl H)) st
( x = w & B . x = Ball (w,r) ) by A16;
hence ex w being Element of (Z | (Cl H)) st C = Ball (w,r) by A31; :: thesis:

end;

hence Z | (Cl H) is totally_bounded ; :: thesis:

end;

assume A32: Z | (Cl H) is totally_bounded ; :: thesis:
thus Z | H is totally_bounded :: thesis:

proof

let r be Real; :: according to TBSP_1:def 1 :: thesis:
assume r > 0 ; :: thesis:
then consider L0 being Subset-Family of (Z | (Cl H)) such that
A33: ( L0 is finite & the carrier of (Z | (Cl H)) = union L0 & ( for C being Subset of (Z | (Cl H)) st C in L0 holds
ex w being Element of (Z | (Cl H)) st C = Ball (w,(r / 2)) ) ) by A32;
A34: for x being object st x in H holds
ex B being Subset of (Z | (Cl H)) st
( x in B & B in L0 )

proof

given x being object such that A35: ( x in H & ( for B being Subset of (Z | (Cl H)) holds
( not x in B or not B in L0 ) ) ) ; :: thesis:
not x in union L0

proof

assume x in union L0 ; :: thesis:
then consider D being set such that
A36: ( x in D & D in L0 ) by TARSKI:def 4;
thus contradiction by A36, A35; :: thesis:

end;

hence contradiction by A2, A35, A4, A33; :: thesis:

end;

set BL = { B where B is Subset of (Z | (Cl H)) : ( B in L0 & H /\ B <> {} ) } ;
consider x being object such that
A37: x in H by XBOOLE_0:def 1;
consider B being Subset of (Z | (Cl H)) such that
A38: ( x in B & B in L0 ) by A34, A37;
B /\ H <> {} by A37, A38, XBOOLE_0:def 4;
then A39: B in { B where B is Subset of (Z | (Cl H)) : ( B in L0 & H /\ B <> {} ) } by A38;
{ B where B is Subset of (Z | (Cl H)) : ( B in L0 & H /\ B <> {} ) } c= L0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { B where B is Subset of (Z | (Cl H)) : ( B in L0 & H /\ B <> {} ) } ; :: thesis:
then ex B being Subset of (Z | (Cl H)) st
( B = x & B in L0 & H /\ B <> {} ) ;
hence x in L0 ; :: thesis:

end;

then reconsider BL = { B where B is Subset of (Z | (Cl H)) : ( B in L0 & H /\ B <> {} ) } as non empty finite set by A39, A33;
defpred S₁[ object , object ] means ex w being Point of (Z | H) ex B being Subset of (Z | (Cl H)) st
( B = $1 & w in B & B in L0 & $2 = Ball (w,r) );
A40: for D being object st D in BL holds
ex w being object st
( w in bool the carrier of (Z | H) & S₁[D,w] )

proof

let D be object ; :: thesis:
assume D in BL ; :: thesis:
then consider B being Subset of (Z | (Cl H)) such that
A41: ( B = D & B in L0 & H /\ B <> {} ) ;
consider x being object such that
A42: x in H /\ B by XBOOLE_0:def 1, A41;
A43: ( x in H & x in B ) by XBOOLE_0:def 4, A42;
reconsider x = x as Point of (Z | H) by A3, XBOOLE_0:def 4, A42;
S₁[D, Ball (x,r)] by A41, A43;
hence ex w being object st
( w in bool the carrier of (Z | H) & S₁[D,w] ) ; :: thesis:

end;

consider U0 being Function of BL,(bool the carrier of (Z | H)) such that
A44: for D being object st D in BL holds
S₁[D,U0 . D] from FUNCT_2:sch 1(A40);
A45: dom U0 = BL by FUNCT_2:def 1;
reconsider L = rng U0 as Subset-Family of (Z | H) ;
take L ; :: thesis:
thus L is finite ; :: thesis:
the carrier of (Z | H) c= union L

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A46: z in the carrier of (Z | H) ; :: thesis:
then consider B being Subset of (Z | (Cl H)) such that
A47: ( z in B & B in L0 ) by A34, A3;
z in H /\ B by A46, A3, A47, XBOOLE_0:def 4;
then A48: B in BL by A47;
then consider w being Point of (Z | H), D being Subset of (Z | (Cl H)) such that
A49: ( D = B & w in D & D in L0 & U0 . B = Ball (w,r) ) by A44;
consider y being Element of (Z | (Cl H)) such that
A50: D = Ball (y,(r / 2)) by A49, A33;
reconsider x = z as Point of (Z | H) by A46;
reconsider x1 = x, w1 = w as Point of (Z | (Cl H)) by A47, A49;
reconsider x2 = x1, w2 = w1 as Point of Z by TOPMETR:def 1, TARSKI:def 3;
x1 in { s where s is Point of (Z | (Cl H)) : dist (y,s) < r / 2 } by METRIC_1:def 14, A47, A49, A50;
then A51: ex s being Point of (Z | (Cl H)) st
( x1 = s & dist (y,s) < r / 2 ) ;
w1 in { s where s is Point of (Z | (Cl H)) : dist (y,s) < r / 2 } by METRIC_1:def 14, A49, A50;
then A52: ex s being Point of (Z | (Cl H)) st
( w1 = s & dist (y,s) < r / 2 ) ;
A53: dist (w1,x1) <= (dist (w1,y)) + (dist (y,x1)) by METRIC_1:4;
(dist (w1,y)) + (dist (y,x1)) < (r / 2) + (r / 2) by A52, A51, XREAL_1:8;
then dist (w1,x1) < r by A53, XXREAL_0:2;
then dist (w2,x2) < r by TOPMETR:def 1;
then dist (w,x) < r by TOPMETR:def 1;
then x in { s where s is Point of (Z | H) : dist (w,s) < r } ;
then A54: z in U0 . B by A49, METRIC_1:def 14;
U0 . B in rng U0 by A48, A45, FUNCT_1:def 3;
hence z in union L by A54, TARSKI:def 4; :: thesis:

end;

hence the carrier of (Z | H) = union L ; :: thesis:
let C be Subset of (Z | H); :: thesis:
assume C in L ; :: thesis:
then consider x being object such that
A55: ( x in dom U0 & C = U0 . x ) by FUNCT_1:def 3;
ex w being Point of (Z | H) ex B being Subset of (Z | (Cl H)) st
( B = x & w in B & B in L0 & U0 . x = Ball (w,r) ) by A44, A55;
hence ex b₁ being Element of the carrier of (Z | H) st C = Ball (b₁,r) by A55; :: thesis:

end;