let N be non empty MetrSpace; :: thesis: for G being Subset-Family of () st G is Cover of () & 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 () st
( w1 in Ga & w2 in Ga & Ga in G ) ) )

let G be Subset-Family of (); :: thesis: ( G is Cover of () & 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 () st
( w1 in Ga & w2 in Ga & Ga in G ) ) ) )

assume that
A1: G is Cover of () 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 () 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 () st
( w1 in Ga & w2 in Ga & Ga in G ) ) )
set TM = TopSpaceMetr N;
defpred S1[ 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 () holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) );
A4: TopSpaceMetr N = TopStruct(# the carrier of 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 () 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 & S1[e,u] )
proof
let e be object ; :: thesis: ( e in NAT implies ex u being object st
( u in the carrier of N & S1[e,u] ) )

assume e in NAT ; :: thesis: ex u being object st
( u in the carrier of N & S1[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 () 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 () 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 & S1[e,u] ) ; :: thesis: verum
end;
ex f being sequence of the carrier of N st
for e being object st e in NAT holds
S1[e,f . e] from 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 () holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ;
defpred S2[ Subset of ()] 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 () such that
A9: for B being Subset of () holds
( B in F iff S2[B] ) from defpred S3[ set ] means ex n being Element of NAT st
( 0 <= n & \$1 = f . n );
set B0 = { x where x is Point of N : S3[x] } ;
A10: { x where x is Point of N : S3[x] } is Subset of N from then A11: { x where x is Point of N : S3[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 )
}
<> {}
proof
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;
reconsider B0 = { x where x is Point of N : S3[x] } as Subset of () by ;
reconsider F = F as Subset-Family of () ;
set G1 = clf F;
A13: Cl B0 in clf F by ;
( clf F <> {} & ( for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds
meet Gd <> {} ) )
proof
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:
reconsider H = H as Subset-Family of () by ;
H is c=-linear
proof
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:
reconsider B = B as Subset of () by A17;
consider V being Subset of () such that
A19: B = Cl V and
A20: V in F by ;
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 ;
reconsider C = C as Subset of () by A18;
consider W being Subset of () such that
A22: C = Cl W and
A23: W in F by ;
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 ;
now :: thesis: ( ( q <= p & V c= W ) or ( p <= q & W c= V ) )
per cases ( q <= p or p <= q ) ;
case A25: q <= p ; :: thesis: V c= W
thus V c= W :: thesis: verum
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 ;
hence y in W by ; :: thesis: verum
end;
end;
case A30: p <= q ; :: thesis: W c= V
thus W c= V :: thesis: verum
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 ;
hence y in V by ; :: thesis: verum
end;
end;
end;
end;
then ( B c= C or C c= B ) by ;
hence B,C are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum
end;
then consider m being set such that
A35: m in H and
A36: for C being set st C in H holds
m c= C by ;
A37: m c= meet H by ;
reconsider m = m as Subset of () by A35;
consider A being Subset of () such that
A38: m = Cl A and
A39: A in F by ;
A <> {} by A9, A12, A39;
then m <> {} by ;
hence meet H <> {} by A37; :: thesis: verum
end;
then ( clf F is closed & clf F is centered ) by ;
then meet (clf F) <> {} by ;
then consider c being Point of () 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 () such that
A41: c in Ge and
A42: Ge in G by ;
reconsider Ge = Ge as Subset of () ;
Ge is open by ;
then consider r being Real such that
A43: r > 0 and
A44: Ball (c,r) c= Ge by ;
reconsider r = r as Real ;
consider n being Nat such that
A45: n > 0 and
A46: 1 / n < r / 2 by ;
reconsider Q1 = Ball (c,(r / 2)) as Subset of () by TOPMETR:12;
A47: Q1 is open by TOPMETR:14;
defpred S4[ set ] means ex n2 being Element of NAT st
( n <= n2 & \$1 = f . n2 );
reconsider B2 = { x where x is Point of () : S4[x] } as Subset of () from A48: n in NAT by ORDINAL1:def 12;
A49: the carrier of () = the carrier of N by TOPMETR:12;
then B2 in F by ;
then Cl B2 in clf F by PCOMPS_1:def 2;
then A50: c in Cl B2 by ;
c in Q1 by ;
then B2 meets Q1 by ;
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 ;
A55: dist (c,y) < r / 2 by ;
1 / n >= 1 / (n + 1) by ;
then A56: 1 / (n + 1) < r / 2 by ;
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 () holds
( not y in Ga or not w2 in Ga or not Ga in G ) by ;
n + 1 <= n2 + 1 by ;
then 1 / (n + 1) >= 1 / (n2 + 1) by XREAL_1:118;
then dist (y,w2) < 1 / (n + 1) by ;
then dist (y,w2) < r / 2 by ;
then A61: (r / 2) + (dist (y,w2)) < (r / 2) + (r / 2) by XREAL_1:6;
r / 1 > r / 2 by ;
then dist (c,y) < r by ;
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 ;
then dist (c,w2) < (r / 2) + (dist (y,w2)) by XXREAL_0:2;
then dist (c,w2) < (r / 2) + (r / 2) by ;
then w2 in Ball (c,r) by METRIC_1:11;
hence contradiction by A42, A44, A62, A60; :: thesis: verum
end;
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 () st
( w1 in Ga & w2 in Ga & Ga in G ) ) ) ; :: thesis: verum