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:217;
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, TBSP_1:def 1;
defpred S₁[ set , set ] means ( $1 in $2 & $2 in G );
A7: for x being set st x in A holds
ex y being set st
( y in bool the carrier of M & S₁[x,y] )

let x be set ; :: thesis:
assume A8: x in A ; :: thesis:
consider y being set such that
A9: ( x in y & y in G ) by A5, A8, 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 A9; :: thesis:

end;

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

let x1, x2 be set ; :: thesis:
assume A11: ( x1 in A & x2 in A & F . x1 = F . x2 ) ; :: thesis:
reconsider p1 = x1, p2 = x2 as Point of M by A11;
F . x1 in G by A10, A11;
then consider w being Point of M such that
A12: F . x1 = Ball w,(r / 2) by A6;
( p1 in Ball w,(r / 2) & p2 in Ball w,(r / 2) ) by A10, A11, A12;
then ( dist p1,w < r / 2 & dist w,p2 < r / 2 & dist p1,p2 <= (dist p1,w) + (dist w,p2) ) by METRIC_1:4, METRIC_1:12;
then ( dist p1,p2 <= (dist p1,w) + (dist w,p2) & (dist p1,w) + (dist w,p2) < (r / 2) + (r / 2) ) by XREAL_1:10;
then dist p1,p2 < (r / 2) + (r / 2) by XXREAL_0:2;
hence x1 = x2 by A3, A11; :: thesis:

end;

then ( F is one-to-one & dom F = A ) by FUNCT_2:25, FUNCT_2:def 1;
then A13: A, rng F are_equipotent by WELLORD2:def 4;
rng F c= G

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in rng F ; :: thesis:
ex y being set st
( y in dom F & x = F . y ) by A14, FUNCT_1:def 5;
hence x in G by A10; :: thesis:

end;

hence A is finite by A13, CARD_1:68, A4; :: thesis:

end;

assume A15: 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 A16: r > 0 ; :: thesis:
consider A being Subset of M such that
A17: for p, q being Point of M st p <> q & p in A & q in A holds
dist p,q >= r and
A18: for p being Point of M ex q being Point of M st
( q in A & p in Ball q,r ) by A16, Th30;
A19: A is finite by A15, A16, A17;
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 } ;
A20: { H₁(p) where p is Point of M : p in A } is finite from FRAENKEL:sch 21(A19);
{ H₁(p) where p is Point of M : p in A } c= bool the carrier of M

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A21: x in { H₁(p) where p is Point of M : p in A } ; :: thesis:
ex p being Point of M st
( x = H₁(p) & p in A ) by A21;
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:
union BA = the carrier of M

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A22: x in the carrier of M ; :: thesis:
reconsider p = x as Point of M by A22;
consider q being Point of M such that
A23: ( q in A & p in H₁(q) ) by A18;
H₁(q) in BA by A23;
hence x in union BA by A23, TARSKI:def 4; :: thesis:

end;

hence union BA = the carrier of M by XBOOLE_0:def 10; :: thesis:

end;

hence ( BA is finite & union BA = the carrier of M ) by A20; :: thesis:
let C be Subset of M; :: thesis:
assume A24: C in BA ; :: thesis:
ex p being Point of M st
( C = H₁(p) & p in A ) by A24;
hence ex b₁ being Element of the carrier of M st C = Ball b₁,r ; :: thesis: