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,() #) 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 ()] 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 () such that
A5: for B being Subset of () holds
( B in F iff S1[B] ) from 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 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 () by A1, A6;
reconsider F = F as Subset-Family of () ;
set G = clf F;
A8: Cl B0 in clf F by ;
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 () 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
A14: B in H and
A15: C in H ; :: thesis:
reconsider B = B, C = C as Subset of () by ;
consider V being Subset of () such that
A16: B = Cl V and
A17: V in F by ;
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 ;
consider W being Subset of () such that
A19: C = Cl W and
A20: W in F by ;
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 ;
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 ;
hence y in W by ; :: 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 ;
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 ; :: 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 ;
A34: m c= meet H by ;
reconsider m = m as Subset of () by ;
consider A being Subset of () such that
A35: m = Cl A and
A36: A in F by ;
A <> {} by A5, A4, A36;
then m <> {} by ;
hence not meet H = {} by A34; :: thesis: verum
end;
clf F is closed by PCOMPS_1:11;
then meet (clf F) <> {} by ;
then consider c being Point of () 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 ;
then A40: c in Ball (c,(r / 2)) by METRIC_1:11;
reconsider Z = Ball (c,(r / 2)) as Subset of () by A1;
Ball (c,(r / 2)) in Family_open_set T by PCOMPS_1:29;
then A41: Z is open by ;
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 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 () by ;
Cl B in clf F by ;
then c in Cl B by ;
then B meets Z by ;
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 ;
A46: g in Z by ;
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 ;
dist ((S2 . n),c) < r / 2 by ;
then A52: (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) < (r / 2) + (r / 2) by ;
dist ((S2 . m),c) <= (dist ((S2 . m),(S2 . n))) + (dist ((S2 . n),c)) by METRIC_1:4;
hence dist ((S2 . m),c) < r by ; :: thesis: verum
end;
hence S2 is convergent ; :: thesis: verum