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 )
assume A2: N is triangle ; :: thesis: ( not TopSpaceMetr N is compact or N is totally_bounded )
set TM = TopSpaceMetr N;
A3: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def 6;
assume A4: TopSpaceMetr N is compact ; :: thesis: N is totally_bounded
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 A5: 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 S₁[ Subset of N] means ex x being Element of N st $1 = Ball x,r;
consider G being Subset-Family of N such that
A6: for C being Subset of N holds
( C in G iff S₁[C] ) from SUBSET_1:sch 3();
reconsider G = G as Subset-Family of (TopSpaceMetr N) by A3;
for C being Subset of (TopSpaceMetr N) st C in G holds
C is open

proof

let C be Subset of (TopSpaceMetr N); :: thesis: ( C in G implies C is open )
assume A7: C in G ; :: thesis: C is open
reconsider C = C as Subset of N by A3;
ex x being Element of N st C = Ball x,r by A6, A7;
then C in the topology of (TopSpaceMetr N) by A2, A3, PCOMPS_1:33;
hence C is open by PRE_TOPC:def 5; :: thesis: verum

end;

then A8: G is open by TOPS_2:def 1;
G is Cover of (TopSpaceMetr N)

proof

for x being Element of (TopSpaceMetr N) holds x in union G

proof

let x be Element of (TopSpaceMetr N); :: thesis: x in union G
reconsider x = x as Element of N by A3;
dist x,x = 0 by A1, METRIC_1:1;
then A9: x in Ball x,r by A5, METRIC_1:12;
Ball x,r in G by A6;
hence x in union G by A9, TARSKI:def 4; :: thesis: verum

end;

then [#] (TopSpaceMetr N) = union G by SUBSET_1:49;
hence G is Cover of (TopSpaceMetr N) by SETFAM_1:60; :: thesis: verum

end;

then consider H being Subset-Family of (TopSpaceMetr N) such that
A10: ( H c= G & H is Cover of (TopSpaceMetr N) & H is finite ) by A4, A8, COMPTS_1:def 3;
reconsider H = H as Subset-Family of N by A3;
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 = [#] (TopSpaceMetr N) by A10, SETFAM_1:60
.= the carrier of (TopSpaceMetr N) ;
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 A3, A6, A10; :: thesis: verum