let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis:
thus ( M is totally_bounded implies for r being Real
for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) holds
A is finite ) :: thesis:

assume A1: M is totally_bounded ; :: thesis:
let r be Real; :: thesis:
let A be Subset of M; :: thesis:
assume that
A2: r > 0 and
A3: for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ; :: thesis:
r / 2 > 0 by A2, XREAL_1:215;
then consider G being Subset-Family of M such that
A4: G is finite and
A5: the carrier of M = union G and
A6: for C being Subset of M st C in G holds
ex w being Point of M st C = Ball (w,(r / 2)) by A1;
defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in D2 & $2 in G );
A7: for x being object st x in A holds
ex y being object st
( y in bool the carrier of M & S₁[x,y] )

let x be object ; :: thesis:
assume x in A ; :: thesis:
then consider y being set such that
A8: x in y and
A9: y in G by A5, TARSKI:def 4;
reconsider y = y as Subset of M by A9;
take y ; :: thesis:
thus ( y in bool the carrier of M & S₁[x,y] ) by A8, A9; :: thesis:

end;

consider F being Function of A,(bool the carrier of M) such that
A10: for x being object st x in A holds
S₁[x,F . x] from FUNCT_2:sch 1(A7);

let x1, x2 be object ; :: thesis:
assume that
A11: x1 in A and
A12: x2 in A and
A13: F . x1 = F . x2 ; :: thesis:
reconsider p1 = x1, p2 = x2 as Point of M by A11, A12;
A14: S₁[x1,F . x1] by A10, A11;
then F . x1 in G ;
then consider w being Point of M such that
A15: F . x1 = Ball (w,(r / 2)) by A6;
p1 in Ball (w,(r / 2)) by A15, A14;
then A16: dist (p1,w) < r / 2 by METRIC_1:11;
A17: dist (p1,p2) <= (dist (p1,w)) + (dist (w,p2)) by METRIC_1:4;
S₁[x2,F . x2] by A10, A12;
then p2 in Ball (w,(r / 2)) by A13, A15;
then dist (w,p2) < r / 2 by METRIC_1:11;
then (dist (p1,w)) + (dist (w,p2)) < (r / 2) + (r / 2) by A16, XREAL_1:8;
then dist (p1,p2) < (r / 2) + (r / 2) by A17, XXREAL_0:2;
hence x1 = x2 by A3, A11, A12; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng F ; :: thesis:
then consider y being object such that
A20: ( y in dom F & x = F . y ) by FUNCT_1:def 3;
S₁[y,F . y] by A10, A20;
then consider D2 being set such that
A21: ( D2 = F . y & y in D2 & F . y in G ) ;
thus x in G by A20, A21; :: thesis:

end;

end;

assume A22: for r being Real
for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) holds
A is finite ; :: thesis:
let r be Real; :: according to TBSP_1:def 1 :: thesis:
assume A23: r > 0 ; :: thesis:
reconsider r = r as Real ;
consider A being Subset of M such that
A24: for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r and
A25: for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) ) by A23, Th29;
deffunc H₁( Point of M) -> Element of bool the carrier of M = Ball ($1,r);
set BA = { H₁(p) where p is Point of M : p in A } ;
A26: A is finite by A22, A23, A24;
A27: { H₁(p) where p is Point of M : p in A } is finite from FRAENKEL:sch 21(A26);
{ H₁(p) where p is Point of M : p in A } c= bool the carrier of M

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { H₁(p) where p is Point of M : p in A } ; :: thesis:
then ex p being Point of M st
( x = H₁(p) & p in A ) ;
hence x in bool the carrier of M ; :: thesis:

end;

then reconsider BA = { H₁(p) where p is Point of M : p in A } as Subset-Family of M ;
take BA ; :: thesis:
the carrier of M c= union BA

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of M ; :: thesis:
then reconsider p = x as Point of M ;
consider q being Point of M such that
A28: q in A and
A29: p in H₁(q) by A25;
H₁(q) in BA by A28;
hence x in union BA by A29, TARSKI:def 4; :: thesis:

end;