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:
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 A6: TopSpaceMetr N = TopStruct(# the carrier of N,() #) by PCOMPS_1:def 5;
then reconsider G = G as Subset-Family of () ;
for x being Element of () holds x in union G
proof
let x be Element of (); :: thesis: x in union G
reconsider x = x as Element of N by A6;
dist (x,x) = 0 by ;
then A7: x in Ball (x,r) by ;
Ball (x,r) in G by A5;
hence x in union G by ; :: thesis: verum
end;
then [#] () = union G by SUBSET_1:28;
then A8: G is Cover of () by SETFAM_1:45;
for C being Subset of () st C in G holds
C is open
proof
let C be Subset of (); :: 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 () by ;
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 () such that
A10: H c= G and
A11: H is Cover of () and
A12: H is finite by ;
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 () by ;
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