let N be non empty MetrSpace; :: thesis: for G being Subset-Family of (TopSpaceMetr N) st G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact holds

ex r being Real st

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) )

let G be Subset-Family of (TopSpaceMetr N); :: thesis: ( G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact implies ex r being Real st

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) ) )

assume that

A1: G is Cover of (TopSpaceMetr N) and

A2: G is open and

A3: TopSpaceMetr N is compact ; :: thesis: ex r being Real st

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) )

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) ) ; :: thesis: verum

ex r being Real st

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) )

let G be Subset-Family of (TopSpaceMetr N); :: thesis: ( G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact implies ex r being Real st

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) ) )

assume that

A1: G is Cover of (TopSpaceMetr N) and

A2: G is open and

A3: TopSpaceMetr N is compact ; :: thesis: ex r being Real st

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) )

now :: thesis: ex r being Real st

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) )

hence
ex r being Real st ( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) )

set TM = TopSpaceMetr N;

defpred S_{1}[ object , object ] means for n being Element of NAT

for w1 being Element of N st n = $1 & w1 = $2 holds

ex w2 being Element of N st

( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) );

A4: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def 5;

assume A5: for r being Real holds

( not r > 0 or ex w1, w2 being Element of N st

( dist (w1,w2) < r & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ) ; :: thesis: contradiction

A6: for e being object st e in NAT holds

ex u being object st

( u in the carrier of N & S_{1}[e,u] )

for e being object st e in NAT holds

S_{1}[e,f . e]
from FUNCT_2:sch 1(A6);

then consider f being sequence of the carrier of N such that

A8: for e being object st e in NAT holds

for n being Element of NAT

for w1 being Element of N st n = e & w1 = f . e holds

ex w2 being Element of N st

( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ;

defpred S_{2}[ Subset of (TopSpaceMetr N)] means ex p being Element of NAT st $1 = { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } ;

consider F being Subset-Family of (TopSpaceMetr N) such that

A9: for B being Subset of (TopSpaceMetr N) holds

( B in F iff S_{2}[B] )
from SUBSET_1:sch 3();

defpred S_{3}[ set ] means ex n being Element of NAT st

( 0 <= n & $1 = f . n );

set B0 = { x where x is Point of N : S_{3}[x] } ;

A10: { x where x is Point of N : S_{3}[x] } is Subset of N
from DOMAIN_1:sch 7();

then A11: { x where x is Point of N : S_{3}[x] } in F
by A4, A9;

A12: for p being Element of NAT holds { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } <> {}_{3}[x] } as Subset of (TopSpaceMetr N) by A4, A10;

reconsider F = F as Subset-Family of (TopSpaceMetr N) ;

set G1 = clf F;

A13: Cl B0 in clf F by A11, PCOMPS_1:def 2;

( clf F <> {} & ( for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds

meet Gd <> {} ) )

then meet (clf F) <> {} by A3, COMPTS_1:4;

then consider c being Point of (TopSpaceMetr N) such that

A40: c in meet (clf F) by SUBSET_1:4;

reconsider c = c as Point of N by A4;

consider Ge being Subset of (TopSpaceMetr N) such that

A41: c in Ge and

A42: Ge in G by A1, PCOMPS_1:3;

reconsider Ge = Ge as Subset of (TopSpaceMetr N) ;

Ge is open by A2, A42, TOPS_2:def 1;

then consider r being Real such that

A43: r > 0 and

A44: Ball (c,r) c= Ge by A41, TOPMETR:15;

reconsider r = r as Real ;

consider n being Nat such that

A45: n > 0 and

A46: 1 / n < r / 2 by A43, Th1, XREAL_1:215;

reconsider Q1 = Ball (c,(r / 2)) as Subset of (TopSpaceMetr N) by TOPMETR:12;

A47: Q1 is open by TOPMETR:14;

defpred S_{4}[ set ] means ex n2 being Element of NAT st

( n <= n2 & $1 = f . n2 );

reconsider B2 = { x where x is Point of (TopSpaceMetr N) : S_{4}[x] } as Subset of (TopSpaceMetr N) from DOMAIN_1:sch 7();

A48: n in NAT by ORDINAL1:def 12;

A49: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12;

then B2 in F by A9, A48;

then Cl B2 in clf F by PCOMPS_1:def 2;

then A50: c in Cl B2 by A40, SETFAM_1:def 1;

c in Q1 by A43, GOBOARD6:1, XREAL_1:215;

then B2 meets Q1 by A50, A47, TOPS_1:12;

then consider x being object such that

A51: x in B2 and

A52: x in Q1 by XBOOLE_0:3;

consider y being Point of N such that

A53: x = y and

A54: ex n2 being Element of NAT st

( n <= n2 & y = f . n2 ) by A49, A51;

A55: dist (c,y) < r / 2 by A52, A53, METRIC_1:11;

1 / n >= 1 / (n + 1) by A45, NAT_1:11, XREAL_1:85;

then A56: 1 / (n + 1) < r / 2 by A46, XXREAL_0:2;

consider n2 being Element of NAT such that

A57: n <= n2 and

A58: y = f . n2 by A54;

consider w2 being Element of N such that

A59: dist (y,w2) < 1 / (n2 + 1) and

A60: for Ga being Subset of (TopSpaceMetr N) holds

( not y in Ga or not w2 in Ga or not Ga in G ) by A8, A58;

n + 1 <= n2 + 1 by A57, XREAL_1:7;

then 1 / (n + 1) >= 1 / (n2 + 1) by XREAL_1:118;

then dist (y,w2) < 1 / (n + 1) by A59, XXREAL_0:2;

then dist (y,w2) < r / 2 by A56, XXREAL_0:2;

then A61: (r / 2) + (dist (y,w2)) < (r / 2) + (r / 2) by XREAL_1:6;

r / 1 > r / 2 by A43, XREAL_1:76;

then dist (c,y) < r by A55, XXREAL_0:2;

then A62: y in Ball (c,r) by METRIC_1:11;

( dist (c,w2) <= (dist (c,y)) + (dist (y,w2)) & (dist (c,y)) + (dist (y,w2)) < (r / 2) + (dist (y,w2)) ) by A55, METRIC_1:4, XREAL_1:6;

then dist (c,w2) < (r / 2) + (dist (y,w2)) by XXREAL_0:2;

then dist (c,w2) < (r / 2) + (r / 2) by A61, XXREAL_0:2;

then w2 in Ball (c,r) by METRIC_1:11;

hence contradiction by A42, A44, A62, A60; :: thesis: verum

end;defpred S

for w1 being Element of N st n = $1 & w1 = $2 holds

ex w2 being Element of N st

( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) );

A4: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def 5;

assume A5: for r being Real holds

( not r > 0 or ex w1, w2 being Element of N st

( dist (w1,w2) < r & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ) ; :: thesis: contradiction

A6: for e being object st e in NAT holds

ex u being object st

( u in the carrier of N & S

proof

ex f being sequence of the carrier of N st
let e be object ; :: thesis: ( e in NAT implies ex u being object st

( u in the carrier of N & S_{1}[e,u] ) )

assume e in NAT ; :: thesis: ex u being object st

( u in the carrier of N & S_{1}[e,u] )

then reconsider m = e as Element of NAT ;

set r = 1 / (m + 1);

consider w1, w2 being Element of N such that

A7: ( dist (w1,w2) < 1 / (m + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) by A5;

for n being Element of NAT

for w4 being Element of N st n = e & w4 = w1 holds

ex w5 being Element of N st

( dist (w4,w5) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w4 in Ga or not w5 in Ga or not Ga in G ) ) ) by A7;

hence ex u being object st

( u in the carrier of N & S_{1}[e,u] )
; :: thesis: verum

end;( u in the carrier of N & S

assume e in NAT ; :: thesis: ex u being object st

( u in the carrier of N & S

then reconsider m = e as Element of NAT ;

set r = 1 / (m + 1);

consider w1, w2 being Element of N such that

A7: ( dist (w1,w2) < 1 / (m + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) by A5;

for n being Element of NAT

for w4 being Element of N st n = e & w4 = w1 holds

ex w5 being Element of N st

( dist (w4,w5) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w4 in Ga or not w5 in Ga or not Ga in G ) ) ) by A7;

hence ex u being object st

( u in the carrier of N & S

for e being object st e in NAT holds

S

then consider f being sequence of the carrier of N such that

A8: for e being object st e in NAT holds

for n being Element of NAT

for w1 being Element of N st n = e & w1 = f . e holds

ex w2 being Element of N st

( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds

( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ;

defpred S

( p <= n & x = f . n ) } ;

consider F being Subset-Family of (TopSpaceMetr N) such that

A9: for B being Subset of (TopSpaceMetr N) holds

( B in F iff S

defpred S

( 0 <= n & $1 = f . n );

set B0 = { x where x is Point of N : S

A10: { x where x is Point of N : S

then A11: { x where x is Point of N : S

A12: for p being Element of NAT holds { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } <> {}

proof

reconsider B0 = { x where x is Point of N : S
let p be Element of NAT ; :: thesis: { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } <> {}

f . p in { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } ;

hence { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } <> {} ; :: thesis: verum

end;( p <= n & x = f . n ) } <> {}

f . p in { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } ;

hence { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } <> {} ; :: thesis: verum

reconsider F = F as Subset-Family of (TopSpaceMetr N) ;

set G1 = clf F;

A13: Cl B0 in clf F by A11, PCOMPS_1:def 2;

( clf F <> {} & ( for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds

meet Gd <> {} ) )

proof

then
( clf F is closed & clf F is centered )
by FINSET_1:def 3, PCOMPS_1:11;
thus
clf F <> {}
by A13; :: thesis: for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds

meet Gd <> {}

let H be set ; :: thesis: ( H <> {} & H c= clf F & H is finite implies meet H <> {} )

assume that

A14: H <> {} and

A15: H c= clf F and

A16: H is finite ; :: thesis: meet H <> {}

reconsider H = H as Subset-Family of (TopSpaceMetr N) by A15, TOPS_2:2;

H is c=-linear

A35: m in H and

A36: for C being set st C in H holds

m c= C by A14, A16, FINSET_1:11;

A37: m c= meet H by A14, A36, SETFAM_1:5;

reconsider m = m as Subset of (TopSpaceMetr N) by A35;

consider A being Subset of (TopSpaceMetr N) such that

A38: m = Cl A and

A39: A in F by A15, A35, PCOMPS_1:def 2;

A <> {} by A9, A12, A39;

then m <> {} by A38, PRE_TOPC:18, XBOOLE_1:3;

hence meet H <> {} by A37; :: thesis: verum

end;meet Gd <> {}

let H be set ; :: thesis: ( H <> {} & H c= clf F & H is finite implies meet H <> {} )

assume that

A14: H <> {} and

A15: H c= clf F and

A16: H is finite ; :: thesis: meet H <> {}

reconsider H = H as Subset-Family of (TopSpaceMetr N) by A15, TOPS_2:2;

H is c=-linear

proof

then consider m being set such that
let B, C be set ; :: according to ORDINAL1:def 8 :: thesis: ( not B in H or not C in H or B,C are_c=-comparable )

assume that

A17: B in H and

A18: C in H ; :: thesis: B,C are_c=-comparable

reconsider B = B as Subset of (TopSpaceMetr N) by A17;

consider V being Subset of (TopSpaceMetr N) such that

A19: B = Cl V and

A20: V in F by A15, A17, PCOMPS_1:def 2;

consider p being Element of NAT such that

A21: V = { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } by A9, A20;

reconsider C = C as Subset of (TopSpaceMetr N) by A18;

consider W being Subset of (TopSpaceMetr N) such that

A22: C = Cl W and

A23: W in F by A15, A18, PCOMPS_1:def 2;

consider q being Element of NAT such that

A24: W = { x where x is Point of N : ex n being Element of NAT st

( q <= n & x = f . n ) } by A9, A23;

hence B,C are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;assume that

A17: B in H and

A18: C in H ; :: thesis: B,C are_c=-comparable

reconsider B = B as Subset of (TopSpaceMetr N) by A17;

consider V being Subset of (TopSpaceMetr N) such that

A19: B = Cl V and

A20: V in F by A15, A17, PCOMPS_1:def 2;

consider p being Element of NAT such that

A21: V = { x where x is Point of N : ex n being Element of NAT st

( p <= n & x = f . n ) } by A9, A20;

reconsider C = C as Subset of (TopSpaceMetr N) by A18;

consider W being Subset of (TopSpaceMetr N) such that

A22: C = Cl W and

A23: W in F by A15, A18, PCOMPS_1:def 2;

consider q being Element of NAT such that

A24: W = { x where x is Point of N : ex n being Element of NAT st

( q <= n & x = f . n ) } by A9, A23;

now :: thesis: ( ( q <= p & V c= W ) or ( p <= q & W c= V ) )end;

then
( B c= C or C c= B )
by A19, A22, PRE_TOPC:19;per cases
( q <= p or p <= q )
;

end;

case A25:
q <= p
; :: thesis: V c= W

thus
V c= W
:: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in V or y in W )

assume y in V ; :: thesis: y in W

then consider x being Point of N such that

A26: y = x and

A27: ex n being Element of NAT st

( p <= n & x = f . n ) by A21;

consider n being Element of NAT such that

A28: p <= n and

A29: x = f . n by A27;

q <= n by A25, A28, XXREAL_0:2;

hence y in W by A24, A26, A29; :: thesis: verum

end;assume y in V ; :: thesis: y in W

then consider x being Point of N such that

A26: y = x and

A27: ex n being Element of NAT st

( p <= n & x = f . n ) by A21;

consider n being Element of NAT such that

A28: p <= n and

A29: x = f . n by A27;

q <= n by A25, A28, XXREAL_0:2;

hence y in W by A24, A26, A29; :: thesis: verum

case A30:
p <= q
; :: thesis: W c= V

thus
W c= V
:: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in W or y in V )

assume y in W ; :: thesis: y in V

then consider x being Point of N such that

A31: y = x and

A32: ex n being Element of NAT st

( q <= n & x = f . n ) by A24;

consider n being Element of NAT such that

A33: q <= n and

A34: x = f . n by A32;

p <= n by A30, A33, XXREAL_0:2;

hence y in V by A21, A31, A34; :: thesis: verum

end;assume y in W ; :: thesis: y in V

then consider x being Point of N such that

A31: y = x and

A32: ex n being Element of NAT st

( q <= n & x = f . n ) by A24;

consider n being Element of NAT such that

A33: q <= n and

A34: x = f . n by A32;

p <= n by A30, A33, XXREAL_0:2;

hence y in V by A21, A31, A34; :: thesis: verum

hence B,C are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

A35: m in H and

A36: for C being set st C in H holds

m c= C by A14, A16, FINSET_1:11;

A37: m c= meet H by A14, A36, SETFAM_1:5;

reconsider m = m as Subset of (TopSpaceMetr N) by A35;

consider A being Subset of (TopSpaceMetr N) such that

A38: m = Cl A and

A39: A in F by A15, A35, PCOMPS_1:def 2;

A <> {} by A9, A12, A39;

then m <> {} by A38, PRE_TOPC:18, XBOOLE_1:3;

hence meet H <> {} by A37; :: thesis: verum

then meet (clf F) <> {} by A3, COMPTS_1:4;

then consider c being Point of (TopSpaceMetr N) such that

A40: c in meet (clf F) by SUBSET_1:4;

reconsider c = c as Point of N by A4;

consider Ge being Subset of (TopSpaceMetr N) such that

A41: c in Ge and

A42: Ge in G by A1, PCOMPS_1:3;

reconsider Ge = Ge as Subset of (TopSpaceMetr N) ;

Ge is open by A2, A42, TOPS_2:def 1;

then consider r being Real such that

A43: r > 0 and

A44: Ball (c,r) c= Ge by A41, TOPMETR:15;

reconsider r = r as Real ;

consider n being Nat such that

A45: n > 0 and

A46: 1 / n < r / 2 by A43, Th1, XREAL_1:215;

reconsider Q1 = Ball (c,(r / 2)) as Subset of (TopSpaceMetr N) by TOPMETR:12;

A47: Q1 is open by TOPMETR:14;

defpred S

( n <= n2 & $1 = f . n2 );

reconsider B2 = { x where x is Point of (TopSpaceMetr N) : S

A48: n in NAT by ORDINAL1:def 12;

A49: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12;

then B2 in F by A9, A48;

then Cl B2 in clf F by PCOMPS_1:def 2;

then A50: c in Cl B2 by A40, SETFAM_1:def 1;

c in Q1 by A43, GOBOARD6:1, XREAL_1:215;

then B2 meets Q1 by A50, A47, TOPS_1:12;

then consider x being object such that

A51: x in B2 and

A52: x in Q1 by XBOOLE_0:3;

consider y being Point of N such that

A53: x = y and

A54: ex n2 being Element of NAT st

( n <= n2 & y = f . n2 ) by A49, A51;

A55: dist (c,y) < r / 2 by A52, A53, METRIC_1:11;

1 / n >= 1 / (n + 1) by A45, NAT_1:11, XREAL_1:85;

then A56: 1 / (n + 1) < r / 2 by A46, XXREAL_0:2;

consider n2 being Element of NAT such that

A57: n <= n2 and

A58: y = f . n2 by A54;

consider w2 being Element of N such that

A59: dist (y,w2) < 1 / (n2 + 1) and

A60: for Ga being Subset of (TopSpaceMetr N) holds

( not y in Ga or not w2 in Ga or not Ga in G ) by A8, A58;

n + 1 <= n2 + 1 by A57, XREAL_1:7;

then 1 / (n + 1) >= 1 / (n2 + 1) by XREAL_1:118;

then dist (y,w2) < 1 / (n + 1) by A59, XXREAL_0:2;

then dist (y,w2) < r / 2 by A56, XXREAL_0:2;

then A61: (r / 2) + (dist (y,w2)) < (r / 2) + (r / 2) by XREAL_1:6;

r / 1 > r / 2 by A43, XREAL_1:76;

then dist (c,y) < r by A55, XXREAL_0:2;

then A62: y in Ball (c,r) by METRIC_1:11;

( dist (c,w2) <= (dist (c,y)) + (dist (y,w2)) & (dist (c,y)) + (dist (y,w2)) < (r / 2) + (dist (y,w2)) ) by A55, METRIC_1:4, XREAL_1:6;

then dist (c,w2) < (r / 2) + (dist (y,w2)) by XXREAL_0:2;

then dist (c,w2) < (r / 2) + (r / 2) by A61, XXREAL_0:2;

then w2 in Ball (c,r) by METRIC_1:11;

hence contradiction by A42, A44, A62, A60; :: thesis: verum

( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds

ex Ga being Subset of (TopSpaceMetr N) st

( w1 in Ga & w2 in Ga & Ga in G ) ) ) ; :: thesis: verum