let N be non empty MetrStruct ; ( N is Reflexive & N is triangle & TopSpaceMetr N is compact implies N is totally_bounded )
assume A1:
N is Reflexive
; ( not N is triangle or not TopSpaceMetr N is compact or N is totally_bounded )
set TM = TopSpaceMetr N;
assume A2:
N is triangle
; ( not TopSpaceMetr N is compact or N is totally_bounded )
assume A3:
TopSpaceMetr N is compact
; N is totally_bounded
let r be Real; TBSP_1:def 1 ( 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
; 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
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
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
; ( 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; verum