let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: ( TopSpaceMetr T is compact implies T is complete )
set TM = TopSpaceMetr T;
A1: TopSpaceMetr T = TopStruct(# the carrier of T,(Family_open_set T) #) by PCOMPS_1:def 5;
assume A2: TopSpaceMetr T is compact ; :: thesis: T is complete
let S2 be sequence of T; :: according to TBSP_1:def 5 :: thesis: ( S2 is Cauchy implies S2 is convergent )
assume A3: S2 is Cauchy ; :: thesis: S2 is convergent
S2 is convergent
proof
A4: for p being Nat holds { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } <> {}
proof
let p be Nat; :: thesis: { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } <> {}
S2 . p in { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } ;
hence { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } <> {} ; :: thesis: verum
end;
defpred S1[ Subset of (TopSpaceMetr T)] means ex p being Nat st $1 = { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } ;
consider F being Subset-Family of (TopSpaceMetr T) such that
A5: for B being Subset of (TopSpaceMetr T) holds
( B in F iff S1[B] ) from SUBSET_1:sch 3();
 defpred S2[ Point of T] means ex n being Nat st
( 0 <= n & $1 = S2 . n );
set B0 = { x where x is Point of T : S2[x] } ;
A6: { x where x is Point of T : S2[x] } is Subset of T from DOMAIN_1:sch 7();
 then A7: { x where x is Point of T : S2[x] } in F by A1, A5;
reconsider B0 = { x where x is Point of T : S2[x] } as Subset of (TopSpaceMetr T) by A1, A6;
reconsider F = F as Subset-Family of (TopSpaceMetr T) ;
set G = clf F;
A8: Cl B0 in clf F by A7, PCOMPS_1:def 2;
A9: clf F is centered
proof
thus clf F <> {} by A8; :: according to FINSET_1:def 3 :: thesis: for b1 being set holds
( b1 = {} or not b1 c= clf F or not b1 is finite or not meet b1 = {} )
let H be set ; :: thesis: ( H = {} or not H c= clf F or not H is finite or not meet H = {} )
assume that
A10: H <> {} and
A11: H c= clf F and
A12: H is finite ; :: thesis: not meet H = {}
A13: H c= bool the carrier of (TopSpaceMetr T) by A11, XBOOLE_1:1;
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
A14: B in H and
A15: C in H ; :: thesis: B,C are_c=-comparable
reconsider B = B, C = C as Subset of (TopSpaceMetr T) by A13, A14, A15;
consider V being Subset of (TopSpaceMetr T) such that
A16: B = Cl V and
A17: V in F by A11, A14, PCOMPS_1:def 2;
consider p being Nat such that
A18: V = { x where x is Point of T : ex n being Nat st
( p <= n & x = S2 . n ) } by A5, A17;
consider W being Subset of (TopSpaceMetr T) such that
A19: C = Cl W and
A20: W in F by A11, A15, PCOMPS_1:def 2;
consider q being Nat such that
A21: W = { x where x is Point of T : ex n being Nat st
( q <= n & x = S2 . n ) } by A5, A20;
now :: thesis: ( ( q <= p & V c= W ) or ( p <= q & W c= V ) )
per cases ( q <= p or p <= q ) ;
case A22: 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 T such that
A23: y = x and
A24: ex n being Nat st
( p <= n & x = S2 . n ) by A18;
consider n being Nat such that
A25: p <= n and
A26: x = S2 . n by A24;
q <= n by A22, A25, XXREAL_0:2;
hence y in W by A21, A23, A26; :: thesis: verum
end;
end;
case A27: 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 T such that
A28: y = x and
A29: ex n being Nat st
( q <= n & x = S2 . n ) by A21;
consider n being Nat such that
A30: q <= n and
A31: x = S2 . n by A29;
p <= n by A27, A30, XXREAL_0:2;
hence y in V by A18, A28, A31; :: thesis: verum
end;
end;
end;
end;
then ( B c= C or C c= B ) by A16, A19, PRE_TOPC:19;
hence B,C are_c=-comparable ; :: thesis: verum
end;
then consider m being set such that
A32: m in H and
A33: for C being set st C in H holds
m c= C by A10, A12, FINSET_1:11;
A34: m c= meet H by A10, A33, SETFAM_1:5;
reconsider m = m as Subset of (TopSpaceMetr T) by A13, A32;
consider A being Subset of (TopSpaceMetr T) such that
A35: m = Cl A and
A36: A in F by A11, A32, PCOMPS_1:def 2;
A <> {} by A5, A4, A36;
then m <> {} by A35, PRE_TOPC:18, XBOOLE_1:3;
hence not meet H = {} by A34; :: thesis: verum
end;
clf F is closed by PCOMPS_1:11;
then meet (clf F) <> {} by A2, A9, COMPTS_1:4;
then consider c being Point of (TopSpaceMetr T) such that
A37: c in meet (clf F) by SUBSET_1:4;
reconsider c = c as Point of T by A1;
take c ; :: according to TBSP_1:def 2 :: thesis: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),c) < r
let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),c) < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),c) < r
then A38: 0 < r / 2 by XREAL_1:215;
then consider p being Nat such that
A39: for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r / 2 by A3;
dist (c,c) < r / 2 by A38, METRIC_1:1;
then A40: c in Ball (c,(r / 2)) by METRIC_1:11;
reconsider Z = Ball (c,(r / 2)) as Subset of (TopSpaceMetr T) by A1;
Ball (c,(r / 2)) in Family_open_set T by PCOMPS_1:29;
then A41: Z is open by A1, PRE_TOPC:def 2;
defpred S3[ set ] means ex n being Nat st
( p <= n & $1 = S2 . n );
set B = { x where x is Point of T : S3[x] } ;
A42: { x where x is Point of T : S3[x] } is Subset of T from DOMAIN_1:sch 7();
 then A43: { x where x is Point of T : S3[x] } in F by A1, A5;
reconsider B = { x where x is Point of T : S3[x] } as Subset of (TopSpaceMetr T) by A1, A42;
Cl B in clf F by A43, PCOMPS_1:def 2;
then c in Cl B by A37, SETFAM_1:def 1;
then B meets Z by A40, A41, PRE_TOPC:def 7;
then consider g being object such that
A44: g in B /\ Z by XBOOLE_0:4;
take p ; :: thesis: for m being Nat st p <= m holds
dist ((S2 . m),c) < r
let m be Nat; :: thesis: ( p <= m implies dist ((S2 . m),c) < r )
A45: g in B by A44, XBOOLE_0:def 4;
A46: g in Z by A44, XBOOLE_0:def 4;
then reconsider g = g as Point of T ;
consider x being Point of T such that
A47: g = x and
A48: ex n being Nat st
( p <= n & x = S2 . n ) by A45;
consider n being Nat such that
A49: p <= n and
A50: x = S2 . n by A48;
assume p <= m ; :: thesis: dist ((S2 . m),c) < r
then A51: dist ((S2 . m),(S2 . n)) < r / 2 by A39, A49;
dist ((S2 . n),c) < r / 2 by A46, A47, A50, METRIC_1:11;
then A52: (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) < (r / 2) + (r / 2) by A51, XREAL_1:8;
dist ((S2 . m),c) <= (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) by METRIC_1:4;
hence dist ((S2 . m),c) < r by A52, XXREAL_0:2; :: thesis: verum
end;
hence S2 is convergent ; :: thesis: verum