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: 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 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 S_{1}[ 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 S_{1}[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 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 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 ; :: 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 (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; :: thesis: verum

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: 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 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 S

consider G being Subset-Family of N such that

A5: for C being Subset of N holds

( C in G iff S

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

proof

then
[#] (TopSpaceMetr N) = union G
by SUBSET_1:28;
let x be Element of (TopSpaceMetr N); :: thesis: x in union G

reconsider x = x as Element of N by A6;

dist (x,x) = 0 by A1, METRIC_1:1;

then A7: x in Ball (x,r) by A4, METRIC_1:11;

Ball (x,r) in G by A5;

hence x in union G by A7, TARSKI:def 4; :: thesis: verum

end;reconsider x = x as Element of N by A6;

dist (x,x) = 0 by A1, METRIC_1:1;

then A7: x in Ball (x,r) by A4, METRIC_1:11;

Ball (x,r) in G by A5;

hence x in union G by A7, TARSKI:def 4; :: thesis: verum

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

proof

then
G is open
by TOPS_2:def 1;
let C be Subset of (TopSpaceMetr N); :: 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 (TopSpaceMetr N) by A2, A6, PCOMPS_1:29;

hence C is open by PRE_TOPC:def 2; :: thesis: verum

end;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 (TopSpaceMetr N) by A2, A6, PCOMPS_1:29;

hence C is open by PRE_TOPC:def 2; :: thesis: verum

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 ; :: 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 (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; :: thesis: verum