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

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

hence
S2 is convergent
; :: thesis: verum
A4:
for p being Nat holds { x where x is Point of T : ex n being Nat st

( p <= n & x = S2 . n ) } <> {}_{1}[ 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 S_{1}[B] )
from SUBSET_1:sch 3();

defpred S_{2}[ Point of T] means ex n being Nat st

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

set B0 = { x where x is Point of T : S_{2}[x] } ;

A6: { x where x is Point of T : S_{2}[x] } is Subset of T
from DOMAIN_1:sch 7();

then A7: { x where x is Point of T : S_{2}[x] } in F
by A1, A5;

reconsider B0 = { x where x is Point of T : S_{2}[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

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 S_{3}[ set ] means ex n being Nat st

( p <= n & $1 = S2 . n );

set B = { x where x is Point of T : S_{3}[x] } ;

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

then A43: { x where x is Point of T : S_{3}[x] } in F
by A1, A5;

reconsider B = { x where x is Point of T : S_{3}[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;( p <= n & x = S2 . n ) } <> {}

proof

defpred S
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;( 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

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

defpred S

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

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

A6: { x where x is Point of T : S

then A7: { x where x is Point of T : S

reconsider B0 = { x where x is Point of T : S

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

clf F is closed
by PCOMPS_1:11;
thus
clf F <> {}
by A8; :: according to FINSET_1:def 3 :: thesis: for b_{1} being set holds

( b_{1} = {} or not b_{1} c= clf F or not b_{1} is finite or not meet b_{1} = {} )

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

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;( b

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

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

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;

hence B,C are_c=-comparable ; :: thesis: verum

end;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 ) )end;

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

end;

case A22:
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 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;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

case A27:
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 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;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

hence B,C are_c=-comparable ; :: thesis: verum

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

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 S

( p <= n & $1 = S2 . n );

set B = { x where x is Point of T : S

A42: { x where x is Point of T : S

then A43: { x where x is Point of T : S

reconsider B = { x where x is Point of T : S

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