:: COMPTS_1 semantic presentation

begin


definition
let T be TopStruct ;
attrT is compact  means :Def1: :: COMPTS_1:def 1
 for F being Subset-Family of T st F is Cover of T & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite );
end;

:: deftheorem Def1 defines compact COMPTS_1:def_1_:_
 for T being TopStruct holds
( T is compact iff for F being Subset-Family of T st F is Cover of T & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) );

definition
let T be non empty TopSpace;
redefine attr T is regular  means :: COMPTS_1:def 2
 for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V );
compatibility
 ( T is regular iff for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) )
proof
thus  ( T is regular implies for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) ) by PRE_TOPC:def_11; ::_thesis: ( ( for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) ) implies T is regular )
assume A1: for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) ; ::_thesis: T is regular
let p be Point of T; :: according to PRE_TOPC:def_11 ::_thesis: for b1 being Element of bool the carrier of T holds
( not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )
let P be Subset of T; ::_thesis: ( not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )
assume that
A2: P is closed and
A3: p in P ` ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
percases ( P = {} or P <> {} ) ;
supposeA4: P = {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
take G1 = [#] T; ::_thesis: ex b1 being Element of bool the carrier of T st
( G1 is open & b1 is open & p in G1 & P c= b1 & G1 misses b1 )
take G2 = {} T; ::_thesis: ( G1 is open & G2 is open & p in G1 & P c= G2 & G1 misses G2 )
thus  ( G1 is open & G2 is open ) ; ::_thesis: ( p in G1 & P c= G2 & G1 misses G2 )
thus  p in G1 ; ::_thesis: ( P c= G2 & G1 misses G2 )
thus  ( P c= G2 & G1 misses G2 ) by A4, XBOOLE_1:65; ::_thesis: verum
end;
suppose P <> {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
hence  ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) by A1, A2, A3; ::_thesis: verum
end;
end;
end;
redefine attr T is normal  means :: COMPTS_1:def 3
 for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q );
compatibility
 ( T is normal iff for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) )
proof
thus  ( T is normal implies for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) by PRE_TOPC:def_12; ::_thesis: ( ( for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) implies T is normal )
assume A5: for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) ; ::_thesis: T is normal
let F1, F2 be Subset of T; :: according to PRE_TOPC:def_12 ::_thesis: ( not F1 is closed or not F2 is closed or not F1 misses F2 or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) )
assume that
A6: F1 is closed and
A7: F2 is closed and
A8: F1 misses F2 ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
percases ( F1 = {} or F2 = {} or ( F1 <> {} & F2 <> {} ) ) ;
supposeA9: F1 = {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
take G1 = {} T; ::_thesis: ex b1 being Element of bool the carrier of T st
( G1 is open & b1 is open & F1 c= G1 & F2 c= b1 & G1 misses b1 )
take G2 = [#] T; ::_thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 )
thus  ( G1 is open & G2 is open ) ; ::_thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 )
thus  F1 c= G1 by A9; ::_thesis: ( F2 c= G2 & G1 misses G2 )
thus  F2 c= G2 ; ::_thesis: G1 misses G2
thus  G1 misses G2 by XBOOLE_1:65; ::_thesis: verum
end;
supposeA10: F2 = {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
take G1 = [#] T; ::_thesis: ex b1 being Element of bool the carrier of T st
( G1 is open & b1 is open & F1 c= G1 & F2 c= b1 & G1 misses b1 )
take G2 = {} T; ::_thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 )
thus  ( G1 is open & G2 is open ) ; ::_thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 )
thus  F1 c= G1 ; ::_thesis: ( F2 c= G2 & G1 misses G2 )
thus  F2 c= G2 by A10; ::_thesis: G1 misses G2
thus  G1 misses G2 by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( F1 <> {} & F2 <> {} ) ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
hence  ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) by A5, A6, A7, A8; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem  defines regular COMPTS_1:def_2_:_
 for T being non empty TopSpace holds
( T is regular iff for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) );

:: deftheorem  defines normal COMPTS_1:def_3_:_
 for T being non empty TopSpace holds
( T is normal iff for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) );

notation
let T be TopStruct ;
synonym  Hausdorff T for  T_2 ;
end;

definition
let T be TopStruct ;
let P be Subset of T;
attrP is compact  means :Def4: :: COMPTS_1:def 4
 for F being Subset-Family of T st F is Cover of P & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite );
end;

:: deftheorem Def4 defines compact COMPTS_1:def_4_:_
 for T being TopStruct
for P being Subset of T holds
( P is compact iff for F being Subset-Family of T st F is Cover of P & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite ) );

registration
let T be TopStruct ;
cluster empty  ->  compact for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is compact
proof
reconsider C = {} as Subset-Family of T by XBOOLE_1:2;
let S be Subset of T; ::_thesis: ( S is empty implies S is compact )
assume  S is empty ; ::_thesis: S is compact
then A1: S c= union C by XBOOLE_1:2;
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of S & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of S & G is finite ) )
assume that
 F is Cover of S and
 F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of S & G is finite )
take  C ; ::_thesis: ( C c= F & C is Cover of S & C is finite )
thus  ( C c= F & C is Cover of S & C is finite ) by A1, SETFAM_1:def_11, XBOOLE_1:2; ::_thesis: verum
end;
end;

theorem Th1: :: COMPTS_1:1
for T being TopStruct holds
( T is compact iff [#] T is compact )
proof
let T be TopStruct ; ::_thesis: ( T is compact iff [#] T is compact )
thus  ( T is compact implies [#] T is compact ) ::_thesis: ( [#] T is compact implies T is compact )
proof
assume A1: T is compact ; ::_thesis: [#] T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of [#] T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of [#] T & G is finite ) )
assume that
A2: F is Cover of [#] T and
A3: F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of [#] T & G is finite )
consider G being Subset-Family of T such that
A4: G c= F and
A5: G is Cover of T and
A6: G is finite by A1, A2, A3, Def1;
take  G ; ::_thesis: ( G c= F & G is Cover of [#] T & G is finite )
thus  ( G c= F & G is Cover of [#] T & G is finite ) by A4, A5, A6; ::_thesis: verum
end;
assume A7: [#] T is compact ; ::_thesis: T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume that
A8: F is Cover of T and
A9: F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
consider G being Subset-Family of T such that
A10: G c= F and
A11: G is Cover of [#] T and
A12: G is finite by A7, A8, A9, Def4;
take  G ; ::_thesis: ( G c= F & G is Cover of T & G is finite )
thus  ( G c= F & G is Cover of T & G is finite ) by A10, A11, A12; ::_thesis: verum
end;

theorem Th2: :: COMPTS_1:2
for T being TopStruct
for A being SubSpace of T
for Q being Subset of T st Q c= [#] A holds
( Q is compact iff for P being Subset of A st P = Q holds
P is compact )
proof
let T be TopStruct ; ::_thesis: for A being SubSpace of T
for Q being Subset of T st Q c= [#] A holds
( Q is compact iff for P being Subset of A st P = Q holds
P is compact )
let A be SubSpace of T; ::_thesis: for Q being Subset of T st Q c= [#] A holds
( Q is compact iff for P being Subset of A st P = Q holds
P is compact )
let Q be Subset of T; ::_thesis: ( Q c= [#] A implies ( Q is compact iff for P being Subset of A st P = Q holds
P is compact ) )
 [#] A c= [#] T by PRE_TOPC:def_4;
then reconsider AA = [#] A as Subset of T ;
assume A1: Q c= [#] A ; ::_thesis: ( Q is compact iff for P being Subset of A st P = Q holds
P is compact )
then A2: Q /\ AA = Q by XBOOLE_1:28;
thus  ( Q is compact implies for P being Subset of A st P = Q holds
P is compact ) ::_thesis: ( ( for P being Subset of A st P = Q holds
P is compact ) implies Q is compact )
proof
assume A3: Q is compact ; ::_thesis: for P being Subset of A st P = Q holds
P is compact
let P be Subset of A; ::_thesis: ( P = Q implies P is compact )
assume A4: P = Q ; ::_thesis: P is compact
thus  P is compact ::_thesis: verum
proof
let G be Subset-Family of A; :: according to COMPTS_1:def_4 ::_thesis: ( G is Cover of P & G is open implies ex G being Subset-Family of A st
( G c= G & G is Cover of P & G is finite ) )
set GG = G;
assume that
A5: G is Cover of P and
A6: G is open ; ::_thesis: ex G being Subset-Family of A st
( G c= G & G is Cover of P & G is finite )
consider F being Subset-Family of T such that
A7: F is open and
A8: for AA being Subset of T st AA = [#] A holds
G = F | AA by A6, TOPS_2:39;
A9: Q c= union G by A4, A5, SETFAM_1:def_11;
 union (F | AA) c= union F by TOPS_2:34;
then  union G c= union F by A8;
then  Q c= union F by A9, XBOOLE_1:1;
then  F is Cover of Q by SETFAM_1:def_11;
then consider F9 being Subset-Family of T such that
A10: F9 c= F and
A11: F9 is Cover of Q and
A12: F9 is finite by A3, A7, Def4;
 F9 | AA c= bool ([#] (T | AA)) ;
then reconsider G9 = F9 | AA as Subset-Family of A by PRE_TOPC:def_5;
take  G9 ; ::_thesis: ( G9 c= G & G9 is Cover of P & G9 is finite )
 F9 | AA c= F | AA by A10, TOPS_2:30;
hence  G9 c= G by A8; ::_thesis: ( G9 is Cover of P & G9 is finite )
 Q c= union F9 by A11, SETFAM_1:def_11;
then  P c= union G9 by A2, A4, TOPS_2:32;
hence  G9 is Cover of P by SETFAM_1:def_11; ::_thesis: G9 is finite
thus  G9 is finite by A12, TOPS_2:36; ::_thesis: verum
end;
end;
thus  ( ( for P being Subset of A st P = Q holds
P is compact ) implies Q is compact ) ::_thesis: verum
proof
reconsider QQ = Q as Subset of A by A1;
assume  for P being Subset of A st P = Q holds
P is compact ; ::_thesis: Q is compact
then A13: QQ is compact ;
thus  Q is compact ::_thesis: verum
proof
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of Q & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of Q & G is finite ) )
set F9 = F;
assume that
A14: F is Cover of Q and
A15: F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of Q & G is finite )
consider f being Function such that
A16: dom f = F and
A17: rng f = F | AA and
A18: for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ AA by TOPS_2:40;
 F | AA c= bool ([#] (T | AA)) ;
then reconsider F9 = rng f as Subset-Family of A by A17, PRE_TOPC:def_5;
A19: F9 is open
proof
let X be Subset of A; :: according to TOPS_2:def_1 ::_thesis: ( not X in F9 or X is open )
assume A20: X in F9 ; ::_thesis: X is open
then reconsider Y = X as Subset of (T | AA) by A17;
consider R being Subset of T such that
A21: R in F and
A22: R /\ AA = Y by A17, A20, TOPS_2:def_3;
 R is open by A15, A21, TOPS_2:def_1;
then  R in the topology of T by PRE_TOPC:def_2;
then  X in the topology of A by A22, PRE_TOPC:def_4;
hence  X is open by PRE_TOPC:def_2; ::_thesis: verum
end;
 Q c= union F by A14, SETFAM_1:def_11;
then  QQ c= union F9 by A2, A17, TOPS_2:32;
then  F9 is Cover of QQ by SETFAM_1:def_11;
then consider G being Subset-Family of A such that
A23: G c= F9 and
A24: G is Cover of QQ and
A25: G is finite by A13, A19, Def4;
consider X being set  such that
A26: X c= dom f and
A27: X is finite and
A28: f .: X = G by A23, A25, ORDERS_1:85;
reconsider G9 = X as Subset-Family of T by A16, A26, TOPS_2:2;
take  G9 ; ::_thesis: ( G9 c= F & G9 is Cover of Q & G9 is finite )
 Q c= union G9
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in union G9 )
assume A29: x in Q ; ::_thesis: x in union G9
 QQ c= union G by A24, SETFAM_1:def_11;
then consider Y being set  such that
A30: x in Y and
A31: Y in G by A29, TARSKI:def_4;
consider z being set  such that
A32: z in dom f and
A33: z in X and
A34: f . z = Y by A28, A31, FUNCT_1:def_6;
reconsider Z = z as Subset of T by A16, A32;
 Y = Z /\ AA by A16, A18, A32, A34;
then  x in Z by A30, XBOOLE_0:def_4;
hence  x in union G9 by A33, TARSKI:def_4; ::_thesis: verum
end;
hence  ( G9 c= F & G9 is Cover of Q & G9 is finite ) by A16, A26, A27, SETFAM_1:def_11; ::_thesis: verum
end;
end;
end;

theorem Th3: :: COMPTS_1:3
for T being TopStruct
for P being Subset of T holds
( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) )
proof
let T be TopStruct ; ::_thesis: for P being Subset of T holds
( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) )
let P be Subset of T; ::_thesis: ( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) )
A1: [#] (T | P) = P by PRE_TOPC:def_5;
hence  ( P = {} implies ( P is compact iff T | P is compact ) ) by Th1; ::_thesis: ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) )
assume that
A2: T is TopSpace-like and
A3: P <> {} ; ::_thesis: ( P is compact iff T | P is compact )
reconsider T9 = T as non empty TopSpace by A2, A3;
reconsider P9 = P as non empty Subset of T9 by A3;
A4: ( [#] (T9 | P9) is compact iff T9 | P9 is compact ) by Th1;
hence  ( P is compact implies T | P is compact ) by A1, Th2; ::_thesis: ( T | P is compact implies P is compact )
assume  T | P is compact ; ::_thesis: P is compact
then  for Q being Subset of (T | P) st Q = P holds
Q is compact by A4, PRE_TOPC:def_5;
hence  P is compact by A1, Th2; ::_thesis: verum
end;

theorem Th4: :: COMPTS_1:4
for T being non empty TopSpace holds
( T is compact iff for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} )
proof
let T be non empty TopSpace; ::_thesis: ( T is compact iff for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} )
thus  ( T is compact implies for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} ) ::_thesis: ( ( for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} ) implies T is compact )
proof
assume A1: T is compact ; ::_thesis: for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {}
let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} )
assume that
A2: F is centered and
A3: F is closed ; ::_thesis: meet F <> {}
reconsider C = COMPLEMENT F as Subset-Family of T ;
assume A4: meet F = {} ; ::_thesis: contradiction
 F <> {} by A2, FINSET_1:def_3;
then  union (COMPLEMENT F) = (meet F) ` by TOPS_2:7
.= [#] T by A4 ;
then A5: COMPLEMENT F is Cover of T by SETFAM_1:def_11;
 COMPLEMENT F is open by A3, TOPS_2:9;
then consider G9 being Subset-Family of T such that
A6: G9 c= C and
A7: G9 is Cover of T and
A8: G9 is finite by A1, A5, Def1;
set F9 = COMPLEMENT G9;
A9: COMPLEMENT G9 is finite by A8, TOPS_2:8;
A10: COMPLEMENT G9 c= F
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in COMPLEMENT G9 or X in F )
assume A11: X in COMPLEMENT G9 ; ::_thesis: X in F
then reconsider X1 = X as Subset of T ;
 X1 ` in G9 by A11, SETFAM_1:def_7;
then  (X1 `) ` in F by A6, SETFAM_1:def_7;
hence  X in F ; ::_thesis: verum
end;
 G9 <> {} by A7, TOPS_2:3;
then A12: COMPLEMENT G9 <> {} by TOPS_2:5;
meet (COMPLEMENT G9) = (union G9) ` by A7, TOPS_2:3, TOPS_2:6
.= ([#] T) \ ([#] T) by A7, SETFAM_1:45
.= {} by XBOOLE_1:37 ;
hence  contradiction by A2, A10, A9, A12, FINSET_1:def_3; ::_thesis: verum
end;
assume A13: for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} ; ::_thesis: T is compact
thus  T is compact ::_thesis: verum
proof
let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume that
A14: F is Cover of T and
A15: F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
reconsider G = COMPLEMENT F as Subset-Family of T ;
A16: G is closed by A15, TOPS_2:10;
 F <> {} by A14, TOPS_2:3;
then A17: G <> {} by TOPS_2:5;
meet G = (union F) ` by A14, TOPS_2:3, TOPS_2:6
.= ([#] T) \ ([#] T) by A14, SETFAM_1:45
.= {} by XBOOLE_1:37 ;
then  not G is centered by A13, A16;
then consider G9 being set  such that
A18: G9 <> {} and
A19: G9 c= G and
A20: G9 is finite and
A21: meet G9 = {} by A17, FINSET_1:def_3;
reconsider G9 = G9 as Subset-Family of T by A19, XBOOLE_1:1;
take F9 = COMPLEMENT G9; ::_thesis: ( F9 c= F & F9 is Cover of T & F9 is finite )
thus  F9 c= F ::_thesis: ( F9 is Cover of T & F9 is finite )
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in F9 or A in F )
assume A22: A in F9 ; ::_thesis: A in F
then reconsider A1 = A as Subset of T ;
 A1 ` in G9 by A22, SETFAM_1:def_7;
then  (A1 `) ` in F by A19, SETFAM_1:def_7;
hence  A in F ; ::_thesis: verum
end;
union F9 = (meet G9) ` by A18, TOPS_2:7
.= [#] T by A21 ;
hence  F9 is Cover of T by SETFAM_1:def_11; ::_thesis: F9 is finite
thus  F9 is finite by A20, TOPS_2:8; ::_thesis: verum
end;
end;

theorem :: COMPTS_1:5
for T being non empty TopSpace holds
( T is compact iff for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) )
proof
let T be non empty TopSpace; ::_thesis: ( T is compact iff for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) )
thus  ( T is compact implies for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) ) ::_thesis: ( ( for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) ) implies T is compact )
proof
assume A1: T is compact ; ::_thesis: for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} )
let F be Subset-Family of T; ::_thesis: ( F <> {} & F is closed & meet F = {} implies ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) )
assume that
A2: F <> {} and
A3: F is closed and
A4: meet F = {} ; ::_thesis: ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} )
 not F is centered by A1, A3, A4, Th4;
then consider G being set  such that
A5: G <> {} and
A6: G c= F and
A7: G is finite and
A8: meet G = {} by A2, FINSET_1:def_3;
reconsider G = G as Subset-Family of T by A6, XBOOLE_1:1;
take  G ; ::_thesis: ( G <> {} & G c= F & G is finite & meet G = {} )
thus  ( G <> {} & G c= F & G is finite & meet G = {} ) by A5, A6, A7, A8; ::_thesis: verum
end;
assume A9: for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) ; ::_thesis: T is compact
 for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {}
proof
let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} )
assume that
A10: F is centered and
A11: F is closed ; ::_thesis: meet F <> {}
assume A12: meet F = {} ; ::_thesis: contradiction
 F <> {} by A10, FINSET_1:def_3;
then  ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) by A9, A11, A12;
hence  contradiction by A10, FINSET_1:def_3; ::_thesis: verum
end;
hence  T is compact by Th4; ::_thesis: verum
end;


theorem Th6: :: COMPTS_1:6
for TS being TopSpace st TS is T_2 holds
for A being Subset of TS st A <> {} & A is compact holds
for p being Point of TS st p in A ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & A c= QS & PS misses QS )
proof
let TS be TopSpace; ::_thesis: ( TS is T_2 implies for A being Subset of TS st A <> {} & A is compact holds
for p being Point of TS st p in A ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & A c= QS & PS misses QS ) )
assume A1: TS is T_2 ; ::_thesis: for A being Subset of TS st A <> {} & A is compact holds
for p being Point of TS st p in A ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & A c= QS & PS misses QS )
let F be Subset of TS; ::_thesis: ( F <> {} & F is compact implies for p being Point of TS st p in F ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & F c= QS & PS misses QS ) )
assume that
A2: F <> {} and
A3: F is compact ; ::_thesis: for p being Point of TS st p in F ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & F c= QS & PS misses QS )
set z = the Element of F;
let a be Point of TS; ::_thesis: ( a in F ` implies ex PS, QS being Subset of TS st
( PS is open & QS is open & a in PS & F c= QS & PS misses QS ) )
assume  a in F ` ; ::_thesis: ex PS, QS being Subset of TS st
( PS is open & QS is open & a in PS & F c= QS & PS misses QS )
then A4: not a in F by XBOOLE_0:def_5;
defpred S1[ set , set , set ] means  ex PS, QS being Subset of TS st
( $2 = PS & $3 = QS & PS is open & QS is open & a in PS & $1 in QS & PS /\ QS = {} );
A5: for x being set st x in F holds
ex y, z being set st
( y in the topology of TS & z in the topology of TS & S1[x,y,z] )
proof
let x be set ; ::_thesis: ( x in F implies ex y, z being set st
( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) )
assume A6: x in F ; ::_thesis: ex y, z being set st
( y in the topology of TS & z in the topology of TS & S1[x,y,z] )
then reconsider p = x as Point of TS ;
consider W, V being Subset of TS such that
A7: W is open and
A8: V is open and
A9: a in W and
A10: p in V and
A11: W misses V by A1, A4, A6, PRE_TOPC:def_10;
reconsider PS = W, QS = V as set ;
take  PS ; ::_thesis: ex z being set st
( PS in the topology of TS & z in the topology of TS & S1[x,PS,z] )
take  QS ; ::_thesis: ( PS in the topology of TS & QS in the topology of TS & S1[x,PS,QS] )
thus  ( PS in the topology of TS & QS in the topology of TS ) by A7, A8, PRE_TOPC:def_2; ::_thesis: S1[x,PS,QS]
take  W ; ::_thesis: ex QS being Subset of TS st
( PS = W & QS = QS & W is open & QS is open & a in W & x in QS & W /\ QS = {} )
take  V ; ::_thesis: ( PS = W & QS = V & W is open & V is open & a in W & x in V & W /\ V = {} )
thus  ( PS = W & QS = V & W is open & V is open & a in W & x in V & W /\ V = {} ) by A7, A8, A9, A10, A11, XBOOLE_0:def_7; ::_thesis: verum
end;
consider f, g being Function such that
A12: ( dom f = F & dom g = F ) and
A13: for x being set st x in F holds
S1[x,f . x,g . x] from MCART_1:sch_1(A5);
 g .: F c= bool the carrier of TS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: F or x in bool the carrier of TS )
assume  x in g .: F ; ::_thesis: x in bool the carrier of TS
then consider y being set  such that
 y in dom g and
A14: y in F and
A15: g . y = x by FUNCT_1:def_6;
 ex PS, QS being Subset of TS st
( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A13, A14;
hence  x in bool the carrier of TS by A15; ::_thesis: verum
end;
then reconsider C = g .: F as Subset-Family of TS ;
A16: C is open
proof
let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in C or G is open )
assume  G in C ; ::_thesis: G is open
then consider x being set  such that
 x in dom g and
A17: x in F and
A18: G = g . x by FUNCT_1:def_6;
 ex PS, QS being Subset of TS st
( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A13, A17;
hence  G is open by A18; ::_thesis: verum
end;
 F c= union C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in union C )
assume A19: x in F ; ::_thesis: x in union C
then consider PS, QS being Subset of TS such that
 f . x = PS and
A20: g . x = QS and
 PS is open and
 QS is open and
 a in PS and
A21: x in QS and
 PS /\ QS = {} by A13;
 QS in C by A12, A19, A20, FUNCT_1:def_6;
hence  x in union C by A21, TARSKI:def_4; ::_thesis: verum
end;
then  C is Cover of F by SETFAM_1:def_11;
then consider C9 being Subset-Family of TS such that
A22: C9 c= C and
A23: C9 is Cover of F and
A24: C9 is finite by A3, A16, Def4;
 C9 c= rng g by A12, A22, RELAT_1:113;
then consider H9 being set  such that
A25: H9 c= dom g and
A26: H9 is finite and
A27: g .: H9 = C9 by A24, ORDERS_1:85;
 f .: H9 c= bool the carrier of TS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: H9 or x in bool the carrier of TS )
assume  x in f .: H9 ; ::_thesis: x in bool the carrier of TS
then consider y being set  such that
 y in dom f and
A28: y in H9 and
A29: f . y = x by FUNCT_1:def_6;
 ex PS, QS being Subset of TS st
( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A12, A13, A25, A28;
hence  x in bool the carrier of TS by A29; ::_thesis: verum
end;
then reconsider B = f .: H9 as Subset-Family of TS ;
take G0 = meet B; ::_thesis: ex QS being Subset of TS st
( G0 is open & QS is open & a in G0 & F c= QS & G0 misses QS )
take G1 = union C9; ::_thesis: ( G0 is open & G1 is open & a in G0 & F c= G1 & G0 misses G1 )
 B is open
proof
let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in B or G is open )
assume  G in B ; ::_thesis: G is open
then consider x being set  such that
A30: x in dom f and
 x in H9 and
A31: G = f . x by FUNCT_1:def_6;
 ex PS, QS being Subset of TS st
( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A12, A13, A30;
hence  G is open by A31; ::_thesis: verum
end;
hence  G0 is open by A26, TOPS_2:20; ::_thesis: ( G1 is open & a in G0 & F c= G1 & G0 misses G1 )
thus  G1 is open by A16, A22, TOPS_2:11, TOPS_2:19; ::_thesis: ( a in G0 & F c= G1 & G0 misses G1 )
A32: for G being set st G in B holds
a in G
proof
let G be set ; ::_thesis: ( G in B implies a in G )
assume A33: G in B ; ::_thesis: a in G
then reconsider G9 = G as Subset of TS ;
consider x being set  such that
A34: x in dom f and
 x in H9 and
A35: G9 = f . x by A33, FUNCT_1:def_6;
 ex PS, QS being Subset of TS st
( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A12, A13, A34;
hence  a in G by A35; ::_thesis: verum
end;
 F c= union C9 by A23, SETFAM_1:def_11;
then  the Element of F in union C9 by A2, TARSKI:def_3;
then consider D being set  such that
 the Element of F in D and
A36: D in C9 by TARSKI:def_4;
reconsider D9 = D as Subset of TS by A36;
consider y being set  such that
A37: y in dom g and
A38: y in H9 and
 D9 = g . y by A27, A36, FUNCT_1:def_6;
 ex PS, QS being Subset of TS st
( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A12, A13, A37;
then  B <> {} by A12, A37, A38, FUNCT_1:def_6;
hence  a in G0 by A32, SETFAM_1:def_1; ::_thesis: ( F c= G1 & G0 misses G1 )
thus  F c= G1 by A23, SETFAM_1:def_11; ::_thesis: G0 misses G1
thus  G0 /\ G1 = {} :: according to XBOOLE_0:def_7 ::_thesis: verum
proof
set x = the Element of (meet B) /\ (union C9);
assume A39: G0 /\ G1 <> {} ; ::_thesis: contradiction
then A40: the Element of (meet B) /\ (union C9) in meet B by XBOOLE_0:def_4;
 the Element of (meet B) /\ (union C9) in union C9 by A39, XBOOLE_0:def_4;
then consider A being set  such that
A41: the Element of (meet B) /\ (union C9) in A and
A42: A in C9 by TARSKI:def_4;
consider z being set  such that
A43: z in dom g and
A44: z in H9 and
A45: A = g . z by A27, A42, FUNCT_1:def_6;
consider PS, QS being Subset of TS such that
A46: f . z = PS and
A47: g . z = QS and
 PS is open and
 QS is open and
 a in PS and
 z in QS and
A48: PS /\ QS = {} by A12, A13, A43;
 PS in B by A12, A43, A44, A46, FUNCT_1:def_6;
then  the Element of (meet B) /\ (union C9) in PS by A40, SETFAM_1:def_1;
hence  contradiction by A41, A45, A47, A48, XBOOLE_0:def_4; ::_thesis: verum
end;
end;

theorem Th7: :: COMPTS_1:7
for TS being TopSpace
for PS being Subset of TS st TS is T_2 & PS is compact holds
PS is closed
proof
let TS be TopSpace; ::_thesis: for PS being Subset of TS st TS is T_2 & PS is compact holds
PS is closed
let PS be Subset of TS; ::_thesis: ( TS is T_2 & PS is compact implies PS is closed )
assume that
A1: TS is T_2 and
A2: PS is compact ; ::_thesis: PS is closed
percases ( PS = {} or PS <> {} ) ;
suppose PS = {} ; ::_thesis: PS is closed
hence  PS is closed ; ::_thesis: verum
end;
supposeA3: PS <> {} ; ::_thesis: PS is closed
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_PS_`_implies_ex_Q_being_Subset_of_TS_st_
(_Q_is_open_&_Q_c=_PS_`_&_a_in_Q_)_)_&_(_ex_Q_being_Subset_of_TS_st_
(_Q_is_open_&_Q_c=_PS_`_&_a_in_Q_)_implies_a_in_PS_`_)_)
let a be set ; ::_thesis: ( ( a in PS ` implies ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q ) ) & ( ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) )
thus  ( a in PS ` implies ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q ) ) ::_thesis: ( ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q ) implies a in PS ` )
proof
assume A4: a in PS ` ; ::_thesis: ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q )
then reconsider p = a as Point of TS ;
consider W, V being Subset of TS such that
A5: W is open and
 V is open and
A6: p in W and
A7: PS c= V and
A8: W misses V by A1, A2, A3, A4, Th6;
take Q = W; ::_thesis: ( Q is open & Q c= PS ` & a in Q )
 W misses (V `) ` by A8;
then A9: W c= V ` by SUBSET_1:24;
 V ` c= PS ` by A7, SUBSET_1:12;
hence  ( Q is open & Q c= PS ` & a in Q ) by A5, A6, A9, XBOOLE_1:1; ::_thesis: verum
end;
thus  ( ex Q being Subset of TS st
( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) ; ::_thesis: verum
end;
then  PS ` is open by TOPS_1:25;
hence  PS is closed by TOPS_1:3; ::_thesis: verum
end;
end;
end;

theorem Th8: :: COMPTS_1:8
for T being TopStruct
for P being Subset of T st T is compact & P is closed holds
P is compact
proof
let T be TopStruct ; ::_thesis: for P being Subset of T st T is compact & P is closed holds
P is compact
let P be Subset of T; ::_thesis: ( T is compact & P is closed implies P is compact )
assume that
A1: T is compact and
A2: P is closed ; ::_thesis: P is compact
reconsider pp = {(P `)} as Subset-Family of T ;
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of P & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite ) )
assume that
A3: F is Cover of P and
A4: F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite )
set FP = F \/ pp;
A5: P ` is open by A2, TOPS_1:3;
A6: F \/ pp is open
proof
let H be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not H in F \/ pp or H is open )
assume  H in F \/ pp ; ::_thesis: H is open
then  ( H in F or H in {(P `)} ) by XBOOLE_0:def_3;
hence  H is open by A4, A5, TARSKI:def_1, TOPS_2:def_1; ::_thesis: verum
end;
reconsider M = {(P `)} as Subset-Family of T ;
 (F \/ {(P `)}) \ {(P `)} = F \ {(P `)} by XBOOLE_1:40;
then A7: (F \/ {(P `)}) \ {(P `)} c= F by XBOOLE_1:36;
 P c= union F by A3, SETFAM_1:def_11;
then  P \/ (P `) c= (union F) \/ (P `) by XBOOLE_1:9;
then  [#] T c= (union F) \/ (P `) by PRE_TOPC:2;
then  [#] T = (union F) \/ (P `) by XBOOLE_0:def_10
.= (union F) \/ (union {(P `)}) by ZFMISC_1:25
.= union (F \/ {(P `)}) by ZFMISC_1:78 ;
then  F \/ pp is Cover of T by SETFAM_1:def_11;
then consider G being Subset-Family of T such that
A8: G c= F \/ pp and
A9: G is Cover of T and
A10: G is finite by A1, A6, Def1;
reconsider G9 = G \ pp as Subset-Family of T ;
take  G9 ; ::_thesis: ( G9 c= F & G9 is Cover of P & G9 is finite )
 G9 c= (F \/ {(P `)}) \ {(P `)} by A8, XBOOLE_1:33;
hence  G9 c= F by A7, XBOOLE_1:1; ::_thesis: ( G9 is Cover of P & G9 is finite )
(union G) \ (union M) = ([#] T) \ (union {(P `)}) by A9, SETFAM_1:45
.= (P `) ` by ZFMISC_1:25
.= P ;
then  P c= union G9 by TOPS_2:4;
hence  G9 is Cover of P by SETFAM_1:def_11; ::_thesis: G9 is finite
thus  G9 is finite by A10; ::_thesis: verum
end;

theorem Th9: :: COMPTS_1:9
for TS being TopSpace
for PS, QS being Subset of TS st PS is compact & QS c= PS & QS is closed holds
QS is compact
proof
let TS be TopSpace; ::_thesis: for PS, QS being Subset of TS st PS is compact & QS c= PS & QS is closed holds
QS is compact
let PS, QS be Subset of TS; ::_thesis: ( PS is compact & QS c= PS & QS is closed implies QS is compact )
assume that
A1: PS is compact and
A2: QS c= PS and
A3: QS is closed ; ::_thesis: QS is compact
percases ( PS = {} or PS <> {} ) ;
suppose PS = {} ; ::_thesis: QS is compact
hence  QS is compact by A2; ::_thesis: verum
end;
suppose PS <> {} ; ::_thesis: QS is compact
then  TS | PS is compact by A1, Th3;
then A4: for QQ being Subset of (TS | PS) st QQ = QS holds
QQ is compact by A3, Th8, TOPS_2:26;
 PS = [#] (TS | PS) by PRE_TOPC:def_5;
hence  QS is compact by A2, A4, Th2; ::_thesis: verum
end;
end;
end;

theorem :: COMPTS_1:10
for T being TopStruct
for P, Q being Subset of T st P is compact & Q is compact holds
P \/ Q is compact
proof
let T be TopStruct ; ::_thesis: for P, Q being Subset of T st P is compact & Q is compact holds
P \/ Q is compact
let P, Q be Subset of T; ::_thesis: ( P is compact & Q is compact implies P \/ Q is compact )
assume that
A1: P is compact and
A2: Q is compact ; ::_thesis: P \/ Q is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of P \/ Q & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of P \/ Q & G is finite ) )
assume that
A3: F is Cover of P \/ Q and
A4: F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of P \/ Q & G is finite )
A5: P \/ Q c= union F by A3, SETFAM_1:def_11;
 Q c= P \/ Q by XBOOLE_1:7;
then  Q c= union F by A5, XBOOLE_1:1;
then  F is Cover of Q by SETFAM_1:def_11;
then consider G2 being Subset-Family of T such that
A6: G2 c= F and
A7: G2 is Cover of Q and
A8: G2 is finite by A2, A4, Def4;
A9: Q c= union G2 by A7, SETFAM_1:def_11;
 P c= P \/ Q by XBOOLE_1:7;
then  P c= union F by A5, XBOOLE_1:1;
then  F is Cover of P by SETFAM_1:def_11;
then consider G1 being Subset-Family of T such that
A10: G1 c= F and
A11: G1 is Cover of P and
A12: G1 is finite by A1, A4, Def4;
reconsider G = G1 \/ G2 as Subset-Family of T ;
take  G ; ::_thesis: ( G c= F & G is Cover of P \/ Q & G is finite )
thus  G c= F by A10, A6, XBOOLE_1:8; ::_thesis: ( G is Cover of P \/ Q & G is finite )
 P c= union G1 by A11, SETFAM_1:def_11;
then  P \/ Q c= (union G1) \/ (union G2) by A9, XBOOLE_1:13;
then  P \/ Q c= union (G1 \/ G2) by ZFMISC_1:78;
hence  G is Cover of P \/ Q by SETFAM_1:def_11; ::_thesis: G is finite
thus  G is finite by A12, A8; ::_thesis: verum
end;

theorem :: COMPTS_1:11
for TS being TopSpace
for PS, QS being Subset of TS st TS is T_2 & PS is compact & QS is compact holds
PS /\ QS is compact
proof
let TS be TopSpace; ::_thesis: for PS, QS being Subset of TS st TS is T_2 & PS is compact & QS is compact holds
PS /\ QS is compact
let PS, QS be Subset of TS; ::_thesis: ( TS is T_2 & PS is compact & QS is compact implies PS /\ QS is compact )
assume that
A1: TS is T_2 and
A2: PS is compact and
A3: QS is compact ; ::_thesis: PS /\ QS is compact
A4: QS is closed by A1, A3, Th7;
 PS is closed by A1, A2, Th7;
hence  PS /\ QS is compact by A2, A4, Th9, XBOOLE_1:17; ::_thesis: verum
end;

theorem :: COMPTS_1:12
for TS being non empty TopSpace st TS is T_2 & TS is compact holds
TS is regular
proof
let TS be non empty TopSpace; ::_thesis: ( TS is T_2 & TS is compact implies TS is regular )
assume that
A1: TS is T_2 and
A2: TS is compact ; ::_thesis: TS is regular
let p be Point of TS; :: according to COMPTS_1:def_2 ::_thesis: for P being Subset of TS st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of TS st
( W is open & V is open & p in W & P c= V & W misses V )
let F be Subset of TS; ::_thesis: ( F <> {} & F is closed & p in F ` implies ex W, V being Subset of TS st
( W is open & V is open & p in W & F c= V & W misses V ) )
assume that
A3: F <> {} and
A4: F is closed and
A5: p in F ` ; ::_thesis: ex W, V being Subset of TS st
( W is open & V is open & p in W & F c= V & W misses V )
thus  ex W, V being Subset of TS st
( W is open & V is open & p in W & F c= V & W misses V ) by A1, A2, A3, A4, A5, Th6, Th8; ::_thesis: verum
end;

theorem :: COMPTS_1:13
for TS being non empty TopSpace st TS is T_2 & TS is compact holds
TS is normal
proof
let TS be non empty TopSpace; ::_thesis: ( TS is T_2 & TS is compact implies TS is normal )
assume that
A1: TS is T_2 and
A2: TS is compact ; ::_thesis: TS is normal
let A, B be Subset of TS; :: according to COMPTS_1:def_3 ::_thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex P, Q being Subset of TS st
( P is open & Q is open & A c= P & B c= Q & P misses Q ) )
assume that
A3: A <> {} and
A4: B <> {} and
A5: A is closed and
A6: B is closed and
A7: A /\ B = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ex P, Q being Subset of TS st
( P is open & Q is open & A c= P & B c= Q & P misses Q )
defpred S1[ set , set , set ] means  ex P, Q being Subset of TS st
( $2 = P & $3 = Q & P is open & Q is open & $1 in P & B c= Q & P /\ Q = {} );
A8: for x being set st x in A holds
ex y, z being set st
( y in the topology of TS & z in the topology of TS & S1[x,y,z] )
proof
let x be set ; ::_thesis: ( x in A implies ex y, z being set st
( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) )
assume A9: x in A ; ::_thesis: ex y, z being set st
( y in the topology of TS & z in the topology of TS & S1[x,y,z] )
then reconsider p = x as Point of TS ;
 not p in B by A7, A9, XBOOLE_0:def_4;
then  p in B ` by SUBSET_1:29;
then consider W, V being Subset of TS such that
A10: W is open and
A11: V is open and
A12: p in W and
A13: B c= V and
A14: W misses V by A1, A2, A4, A6, Th6, Th8;
reconsider X = W, Y = V as set ;
take  X ; ::_thesis: ex z being set st
( X in the topology of TS & z in the topology of TS & S1[x,X,z] )
take  Y ; ::_thesis: ( X in the topology of TS & Y in the topology of TS & S1[x,X,Y] )
thus  ( X in the topology of TS & Y in the topology of TS ) by A10, A11, PRE_TOPC:def_2; ::_thesis: S1[x,X,Y]
 W /\ V = {} by A14, XBOOLE_0:def_7;
hence  S1[x,X,Y] by A10, A11, A12, A13; ::_thesis: verum
end;
consider f, g being Function such that
A15: ( dom f = A & dom g = A ) and
A16: for x being set st x in A holds
S1[x,f . x,g . x] from MCART_1:sch_1(A8);
 f .: A c= bool the carrier of TS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: A or x in bool the carrier of TS )
assume  x in f .: A ; ::_thesis: x in bool the carrier of TS
then consider y being set  such that
 y in dom f and
A17: y in A and
A18: f . y = x by FUNCT_1:def_6;
 ex P, Q being Subset of TS st
( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A16, A17;
hence  x in bool the carrier of TS by A18; ::_thesis: verum
end;
then reconsider Cf = f .: A as Subset-Family of TS ;
 A c= union Cf
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union Cf )
assume A19: x in A ; ::_thesis: x in union Cf
then consider P, Q being Subset of TS such that
A20: f . x = P and
 g . x = Q and
 P is open and
 Q is open and
A21: x in P and
 B c= Q and
 P /\ Q = {} by A16;
 P in Cf by A15, A19, A20, FUNCT_1:def_6;
hence  x in union Cf by A21, TARSKI:def_4; ::_thesis: verum
end;
then A22: Cf is Cover of A by SETFAM_1:def_11;
A23: Cf is open
proof
let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in Cf or G is open )
assume  G in Cf ; ::_thesis: G is open
then consider x being set  such that
 x in dom f and
A24: x in A and
A25: G = f . x by FUNCT_1:def_6;
 ex P, Q being Subset of TS st
( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A16, A24;
hence  G is open by A25; ::_thesis: verum
end;
 A is compact by A2, A5, Th8;
then consider C being Subset-Family of TS such that
A26: C c= Cf and
A27: C is Cover of A and
A28: C is finite by A22, A23, Def4;
set z = the Element of A;
 A c= union C by A27, SETFAM_1:def_11;
then  the Element of A in union C by A3, TARSKI:def_3;
then consider D being set  such that
 the Element of A in D and
A29: D in C by TARSKI:def_4;
 C c= rng f by A15, A26, RELAT_1:113;
then consider H9 being set  such that
A30: H9 c= dom f and
A31: H9 is finite and
A32: f .: H9 = C by A28, ORDERS_1:85;
 g .: H9 c= bool the carrier of TS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: H9 or x in bool the carrier of TS )
assume  x in g .: H9 ; ::_thesis: x in bool the carrier of TS
then consider y being set  such that
 y in dom g and
A33: y in H9 and
A34: g . y = x by FUNCT_1:def_6;
 ex P, Q being Subset of TS st
( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A30, A33;
hence  x in bool the carrier of TS by A34; ::_thesis: verum
end;
then reconsider Bk = g .: H9 as Subset-Family of TS ;
consider y being set  such that
A35: y in dom f and
A36: y in H9 and
 D = f . y by A32, A29, FUNCT_1:def_6;
A37: for X being set st X in Bk holds
B c= X
proof
let X be set ; ::_thesis: ( X in Bk implies B c= X )
assume A38: X in Bk ; ::_thesis: B c= X
then reconsider X9 = X as Subset of TS ;
consider x being set  such that
A39: x in dom g and
 x in H9 and
A40: X9 = g . x by A38, FUNCT_1:def_6;
 ex P, Q being Subset of TS st
( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A39;
hence  B c= X by A40; ::_thesis: verum
end;
take W = union C; ::_thesis: ex Q being Subset of TS st
( W is open & Q is open & A c= W & B c= Q & W misses Q )
take V = meet Bk; ::_thesis: ( W is open & V is open & A c= W & B c= V & W misses V )
thus  W is open by A23, A26, TOPS_2:11, TOPS_2:19; ::_thesis: ( V is open & A c= W & B c= V & W misses V )
 Bk is open
proof
let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in Bk or G is open )
assume  G in Bk ; ::_thesis: G is open
then consider x being set  such that
A41: x in dom g and
 x in H9 and
A42: G = g . x by FUNCT_1:def_6;
 ex P, Q being Subset of TS st
( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A41;
hence  G is open by A42; ::_thesis: verum
end;
hence  V is open by A31, TOPS_2:20; ::_thesis: ( A c= W & B c= V & W misses V )
thus  A c= W by A27, SETFAM_1:def_11; ::_thesis: ( B c= V & W misses V )
 ex P, Q being Subset of TS st
( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A35;
then  Bk <> {} by A15, A35, A36, FUNCT_1:def_6;
hence  B c= V by A37, SETFAM_1:5; ::_thesis: W misses V
thus  W /\ V = {} :: according to XBOOLE_0:def_7 ::_thesis: verum
proof
set x = the Element of (union C) /\ (meet Bk);
assume A43: W /\ V <> {} ; ::_thesis: contradiction
then A44: the Element of (union C) /\ (meet Bk) in meet Bk by XBOOLE_0:def_4;
 the Element of (union C) /\ (meet Bk) in union C by A43, XBOOLE_0:def_4;
then consider D being set  such that
A45: the Element of (union C) /\ (meet Bk) in D and
A46: D in C by TARSKI:def_4;
consider z being set  such that
A47: z in dom f and
A48: z in H9 and
A49: D = f . z by A32, A46, FUNCT_1:def_6;
consider P, Q being Subset of TS such that
A50: f . z = P and
A51: g . z = Q and
 P is open and
 Q is open and
 z in P and
 B c= Q and
A52: P /\ Q = {} by A15, A16, A47;
 Q in Bk by A15, A47, A48, A51, FUNCT_1:def_6;
then  the Element of (union C) /\ (meet Bk) in Q by A44, SETFAM_1:def_1;
hence  contradiction by A45, A49, A50, A52, XBOOLE_0:def_4; ::_thesis: verum
end;
end;


theorem :: COMPTS_1:14
for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds
S is compact
proof
let T be TopStruct ; ::_thesis: for S being non empty TopStruct
for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds
S is compact
let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds
S is compact
let f be Function of T,S; ::_thesis: ( T is compact & f is continuous & rng f = [#] S implies S is compact )
assume A1: T is compact ; ::_thesis: ( not f is continuous or not rng f = [#] S or S is compact )
 [#] T c= dom f by FUNCT_2:def_1;
then A2: [#] T c= f " (f .: ([#] T)) by FUNCT_1:76;
assume that
A3: f is continuous and
A4: rng f = [#] S ; ::_thesis: S is compact
let F be Subset-Family of S; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of S & F is open implies ex G being Subset-Family of S st
( G c= F & G is Cover of S & G is finite ) )
assume that
A5: F is Cover of S and
A6: F is open ; ::_thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of S & G is finite )
set F1 = F;
reconsider G = (" f) .: F as Subset-Family of T by TOPS_2:42;
union G = f " (union F) by A4, FUNCT_3:26
.= f " (rng f) by A4, A5, SETFAM_1:45
.= f " (f .: (dom f)) by RELAT_1:113
.= f " (f .: ([#] T)) by FUNCT_2:def_1 ;
then A7: G is Cover of T by A2, SETFAM_1:def_11;
A8: (.: f) .: ((.: f) " F) c= F by FUNCT_1:75;
 (.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by FUNCT_3:29, RELAT_1:123;
then A9: (.: f) .: G c= F by A8, XBOOLE_1:1;
 G is open by A3, A6, TOPS_2:47;
then consider G9 being Subset-Family of T such that
A10: G9 c= G and
A11: G9 is Cover of T and
A12: G9 is finite by A1, A7, Def1;
reconsider F9 = (.: f) .: G9 as Subset-Family of S ;
take  F9 ; ::_thesis: ( F9 c= F & F9 is Cover of S & F9 is finite )
 (.: f) .: G9 c= (.: f) .: G by A10, RELAT_1:123;
hence  F9 c= F by A9, XBOOLE_1:1; ::_thesis: ( F9 is Cover of S & F9 is finite )
 dom f = [#] T by FUNCT_2:def_1;
then  union F9 = f .: (union G9) by FUNCT_3:14
.= f .: ([#] T) by A11, SETFAM_1:45
.= f .: (dom f) by FUNCT_2:def_1
.= [#] S by A4, RELAT_1:113 ;
hence  F9 is Cover of S by SETFAM_1:def_11; ::_thesis: F9 is finite
thus  F9 is finite by A12; ::_thesis: verum
end;

theorem Th15: :: COMPTS_1:15
for T being TopStruct
for P being Subset of T
for S being non empty TopStruct
for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds
f .: P is compact
proof
let T be TopStruct ; ::_thesis: for P being Subset of T
for S being non empty TopStruct
for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds
f .: P is compact
let P be Subset of T; ::_thesis: for S being non empty TopStruct
for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds
f .: P is compact
let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds
f .: P is compact
let f be Function of T,S; ::_thesis: ( f is continuous & rng f = [#] S & P is compact implies f .: P is compact )
assume that
A1: f is continuous and
A2: rng f = [#] S and
A3: P is compact ; ::_thesis: f .: P is compact
let F be Subset-Family of S; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of f .: P & F is open implies ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) )
assume that
A4: F is Cover of f .: P and
A5: F is open ; ::_thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
reconsider G = (" f) .: F as Subset-Family of T by TOPS_2:42;
 f .: P c= union F by A4, SETFAM_1:def_11;
then A6: f " (f .: P) c= f " (union F) by RELAT_1:143;
 P c= [#] T ;
then  P c= dom f by FUNCT_2:def_1;
then A7: P c= f " (f .: P) by FUNCT_1:76;
 union G = f " (union F) by A2, FUNCT_3:26;
then  P c= union G by A6, A7, XBOOLE_1:1;
then A8: G is Cover of P by SETFAM_1:def_11;
 G is open by A1, A5, TOPS_2:47;
then consider G9 being Subset-Family of T such that
A9: G9 c= G and
A10: G9 is Cover of P and
A11: G9 is finite by A3, A8, Def4;
reconsider F9 = (.: f) .: G9 as Subset-Family of S ;
take  F9 ; ::_thesis: ( F9 c= F & F9 is Cover of f .: P & F9 is finite )
A12: (.: f) .: ((.: f) " F) c= F by FUNCT_1:75;
 (.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by FUNCT_3:29, RELAT_1:123;
then A13: (.: f) .: G c= F by A12, XBOOLE_1:1;
 (.: f) .: G9 c= (.: f) .: G by A9, RELAT_1:123;
hence  F9 c= F by A13, XBOOLE_1:1; ::_thesis: ( F9 is Cover of f .: P & F9 is finite )
A14: P c= union G9 by A10, SETFAM_1:def_11;
 dom f = [#] T by FUNCT_2:def_1;
then  union F9 = f .: (union G9) by FUNCT_3:14;
then  f .: P c= union F9 by A14, RELAT_1:123;
hence  F9 is Cover of f .: P by SETFAM_1:def_11; ::_thesis: F9 is finite
thus  F9 is finite by A11; ::_thesis: verum
end;


theorem Th16: :: COMPTS_1:16
for TS being TopSpace
for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds
for PS being Subset of TS st PS is closed holds
f .: PS is closed
proof
let TS be TopSpace; ::_thesis: for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds
for PS being Subset of TS st PS is closed holds
f .: PS is closed
let SS be non empty TopSpace; ::_thesis: for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds
for PS being Subset of TS st PS is closed holds
f .: PS is closed
let f be Function of TS,SS; ::_thesis: ( TS is compact & SS is T_2 & rng f = [#] SS & f is continuous implies for PS being Subset of TS st PS is closed holds
f .: PS is closed )
assume that
A1: TS is compact and
A2: SS is T_2 and
A3: rng f = [#] SS and
A4: f is continuous ; ::_thesis: for PS being Subset of TS st PS is closed holds
f .: PS is closed
let PS be Subset of TS; ::_thesis: ( PS is closed implies f .: PS is closed )
assume  PS is closed ; ::_thesis: f .: PS is closed
then  PS is compact by A1, Th8;
hence  f .: PS is closed by A2, A3, A4, Th7, Th15; ::_thesis: verum
end;

theorem :: COMPTS_1:17
for TS being TopSpace
for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds
f is being_homeomorphism
proof
let TS be TopSpace; ::_thesis: for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds
f is being_homeomorphism
let SS be non empty TopSpace; ::_thesis: for f being Function of TS,SS st TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds
f is being_homeomorphism
let f be Function of TS,SS; ::_thesis: ( TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous implies f is being_homeomorphism )
assume that
A1: TS is compact and
A2: SS is T_2 and
A3: dom f = [#] TS and
A4: rng f = [#] SS and
A5: f is one-to-one and
A6: f is continuous ; ::_thesis: f is being_homeomorphism
 for P being Subset of TS holds
( P is closed iff f .: P is closed )
proof
let P be Subset of TS; ::_thesis: ( P is closed iff f .: P is closed )
 dom f = [#] TS by FUNCT_2:def_1;
then A7: P c= f " (f .: P) by FUNCT_1:76;
thus  ( P is closed implies f .: P is closed ) by A1, A2, A4, A6, Th16; ::_thesis: ( f .: P is closed implies P is closed )
assume  f .: P is closed ; ::_thesis: P is closed
then A8: f " (f .: P) is closed by A6, PRE_TOPC:def_6;
 f " (f .: P) c= P by A5, FUNCT_1:82;
hence  P is closed by A8, A7, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  f is being_homeomorphism by A3, A4, A5, TOPS_2:58; ::_thesis: verum
end;

definition
let D be set ;
func 1TopSp D ->  TopStruct  equals :: COMPTS_1:def 5
 TopStruct(# D,([#] (bool D)) #);
coherence
 TopStruct(# D,([#] (bool D)) #) is TopStruct ;
end;

:: deftheorem  defines 1TopSp COMPTS_1:def_5_:_
 for D being set holds 1TopSp D = TopStruct(# D,([#] (bool D)) #);

registration
let D be set ;
cluster 1TopSp D ->  strict TopSpace-like ;
coherence
 ( 1TopSp D is strict & 1TopSp D is TopSpace-like )
proof
thus  1TopSp D is strict ; ::_thesis: 1TopSp D is TopSpace-like
set T = 1TopSp D;
A1: for X being Subset-Family of (1TopSp D) st X c= the topology of (1TopSp D) holds
union X in the topology of (1TopSp D) ;
A2: for p, q being Subset of (1TopSp D) st p in the topology of (1TopSp D) & q in the topology of (1TopSp D) holds
p /\ q in the topology of (1TopSp D) ;
 D in bool D by ZFMISC_1:def_1;
hence  1TopSp D is TopSpace-like by A1, A2, PRE_TOPC:def_1; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
cluster 1TopSp D ->  non empty ;
coherence
 not 1TopSp D is empty ;
end;

registration
let x be set ;
cluster 1TopSp {x} ->  T_2 ;
coherence
 1TopSp {x} is Hausdorff
proof
let p, q be Point of (1TopSp {x}); :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of (1TopSp {x}) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A1: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of (1TopSp {x}) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
 p = x by TARSKI:def_1;
hence  ex b1, b2 being Element of bool the carrier of (1TopSp {x}) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A1, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like T_2 for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is T_2 & not b1 is empty )
proof
take  1TopSp {{}} ; ::_thesis: ( 1TopSp {{}} is T_2 & not 1TopSp {{}} is empty )
thus  ( 1TopSp {{}} is T_2 & not 1TopSp {{}} is empty ) ; ::_thesis: verum
end;
end;

registration
let T be non empty T_2 TopSpace;
cluster compact  ->  closed for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is compact holds
b1 is closed by Th7;
end;

registration
let A be finite set ;
cluster 1TopSp A ->  finite ;
coherence
 1TopSp A is finite ;
end;

registration
cluster non empty finite strict TopSpace-like for TopStruct ;
existence
 ex b1 being TopSpace st
( not b1 is empty & b1 is finite & b1 is strict )
proof
take  1TopSp {{}} ; ::_thesis: ( not 1TopSp {{}} is empty & 1TopSp {{}} is finite & 1TopSp {{}} is strict )
thus  ( not 1TopSp {{}} is empty & 1TopSp {{}} is finite & 1TopSp {{}} is strict ) ; ::_thesis: verum
end;
end;

registration
cluster finite TopSpace-like  ->  compact for TopStruct ;
coherence
 for b1 being TopSpace st b1 is finite holds
b1 is compact
proof
let T be TopSpace; ::_thesis: ( T is finite implies T is compact )
assume A1: the carrier of T is finite ; :: according to STRUCT_0:def_11 ::_thesis: T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume that
A2: F is Cover of T and
 F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
take  F ; ::_thesis: ( F c= F & F is Cover of T & F is finite )
thus  ( F c= F & F is Cover of T ) by A2; ::_thesis: F is finite
thus  F is finite by A1; ::_thesis: verum
end;
end;

theorem Th18: :: COMPTS_1:18
for T being TopSpace st the carrier of T is finite holds
T is compact
proof
let T be TopSpace; ::_thesis: ( the carrier of T is finite implies T is compact )
assume  the carrier of T is finite ; ::_thesis: T is compact
then  T is finite ;
hence  T is compact ; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster finite  ->  compact for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is finite holds
b1 is compact
proof
let A be Subset of T; ::_thesis: ( A is finite implies A is compact )
assume  A is finite ; ::_thesis: A is compact
then reconsider B = A as finite Subset of T ;
 [#] (T | B) = B by PRE_TOPC:def_5;
then A1: T | B is compact by Th18;
 ( B = {} or B <> {} ) ;
hence  A is compact by A1, Th3; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
cluster non empty compact for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st
( not b1 is empty & b1 is compact )
proof
set A = the non empty finite Subset of T;
take  the non empty finite Subset of T ; ::_thesis: ( not the non empty finite Subset of T is empty & the non empty finite Subset of T is compact )
thus  ( not the non empty finite Subset of T is empty & the non empty finite Subset of T is compact ) ; ::_thesis: verum
end;
end;

registration
cluster empty  ->  T_2 for TopStruct ;
coherence
 for b1 being TopStruct st b1 is empty holds
b1 is T_2
proof
let T be TopStruct ; ::_thesis: ( T is empty implies T is T_2 )
assume A1: T is empty ; ::_thesis: T is T_2
let p, q be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
thus  ( p = q or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) by A1, STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
let T be T_2 TopStruct ;
cluster  ->  T_2 for SubSpace of T;
coherence
 for b1 being SubSpace of T holds b1 is T_2
proof
let A be SubSpace of T; ::_thesis: A is T_2
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: A is T_2
hence  A is T_2 ; ::_thesis: verum
end;
supposeA1: not A is empty ; ::_thesis: A is T_2
let p, q be Point of A; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of A st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A2: not p = q ; ::_thesis: ex b1, b2 being Element of bool the carrier of A st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
 [#] A c= [#] T by PRE_TOPC:def_4;
then  not T is empty by A1;
then reconsider p9 = p, q9 = q as Point of T by A1, PRE_TOPC:25;
consider W, V being Subset of T such that
A3: W is open and
A4: V is open and
A5: p9 in W and
A6: q9 in V and
A7: W misses V by A2, PRE_TOPC:def_10;
reconsider W9 = W /\ ([#] A), V9 = V /\ ([#] A) as Subset of A ;
 V in the topology of T by A4, PRE_TOPC:def_2;
then A8: V9 in the topology of A by PRE_TOPC:def_4;
take  W9 ; ::_thesis: ex b1 being Element of bool the carrier of A st
( W9 is open & b1 is open & p in W9 & q in b1 & W9 misses b1 )
take  V9 ; ::_thesis: ( W9 is open & V9 is open & p in W9 & q in V9 & W9 misses V9 )
 W in the topology of T by A3, PRE_TOPC:def_2;
then  W9 in the topology of A by PRE_TOPC:def_4;
hence  ( W9 is open & V9 is open ) by A8, PRE_TOPC:def_2; ::_thesis: ( p in W9 & q in V9 & W9 misses V9 )
thus  ( p in W9 & q in V9 ) by A1, A5, A6, XBOOLE_0:def_4; ::_thesis: W9 misses V9
A9: W /\ V = {} by A7, XBOOLE_0:def_7;
W9 /\ V9 = (W /\ (V /\ ([#] A))) /\ ([#] A) by XBOOLE_1:16
.= {} /\ ([#] A) by A9, XBOOLE_1:16
.= {} ;
hence  W9 misses V9 by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
end;

theorem Th19: :: COMPTS_1:19
for X being TopStruct
for Y being SubSpace of X
for A being Subset of X
for B being Subset of Y st A = B holds
( A is compact iff B is compact )
proof
let X be TopStruct ; ::_thesis: for Y being SubSpace of X
for A being Subset of X
for B being Subset of Y st A = B holds
( A is compact iff B is compact )
let Y be SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y st A = B holds
( A is compact iff B is compact )
let A be Subset of X; ::_thesis: for B being Subset of Y st A = B holds
( A is compact iff B is compact )
let B be Subset of Y; ::_thesis: ( A = B implies ( A is compact iff B is compact ) )
assume A1: A = B ; ::_thesis: ( A is compact iff B is compact )
A2: B c= [#] Y ;
hence  ( A is compact implies B is compact ) by A1, Th2; ::_thesis: ( B is compact implies A is compact )
assume  B is compact ; ::_thesis: A is compact
then  for P being Subset of Y st P = A holds
P is compact by A1;
hence  A is compact by A1, A2, Th2; ::_thesis: verum
end;


theorem :: COMPTS_1:20
for T, S being non empty TopSpace
for p being Point of T
for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds
f +* g is continuous Function of T,S
proof
let T, S be non empty TopSpace; ::_thesis: for p being Point of T
for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds
f +* g is continuous Function of T,S
let p be Point of T; ::_thesis: for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds
f +* g is continuous Function of T,S
let T1, T2 be SubSpace of T; ::_thesis: for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds
f +* g is continuous Function of T,S
let f be Function of T1,S; ::_thesis: for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds
f +* g is continuous Function of T,S
let g be Function of T2,S; ::_thesis: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p implies f +* g is continuous Function of T,S )
assume that
A1: ([#] T1) \/ ([#] T2) = [#] T and
A2: ([#] T1) /\ ([#] T2) = {p} and
A3: T1 is compact and
A4: T2 is compact and
A5: T is T_2 and
A6: f is continuous and
A7: g is continuous and
A8: f . p = g . p ; ::_thesis: f +* g is continuous Function of T,S
set h = f +* g;
A9: dom g = [#] T2 by FUNCT_2:def_1;
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then A10: rng (f +* g) c= the carrier of S by XBOOLE_1:1;
A11: dom f = [#] T1 by FUNCT_2:def_1;
then  dom (f +* g) = the carrier of T by A1, A9, FUNCT_4:def_1;
then reconsider h = f +* g as Function of T,S by A10, FUNCT_2:def_1, RELSET_1:4;
 for P being Subset of S st P is closed holds
h " P is closed
proof
let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed )
 [#] T1 c= [#] T by A1, XBOOLE_1:7;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
 [#] T2 c= [#] T by A1, XBOOLE_1:7;
then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;
A12: dom h = (dom f) \/ (dom g) by FUNCT_4:def_1;
A13: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_T2)_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_T2)_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )
thus  ( x in (h " P) /\ ([#] T2) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) )
proof
assume A14: x in (h " P) /\ ([#] T2) ; ::_thesis: x in g " P
then  x in h " P by XBOOLE_0:def_4;
then A15: h . x in P by FUNCT_1:def_7;
 g . x = h . x by A9, A14, FUNCT_4:13;
hence  x in g " P by A9, A14, A15, FUNCT_1:def_7; ::_thesis: verum
end;
assume A16: x in g " P ; ::_thesis: x in (h " P) /\ ([#] T2)
then A17: x in dom g by FUNCT_1:def_7;
 g . x in P by A16, FUNCT_1:def_7;
then A18: h . x in P by A17, FUNCT_4:13;
 x in dom h by A12, A17, XBOOLE_0:def_3;
then  x in h " P by A18, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] T2) by A16, XBOOLE_0:def_4; ::_thesis: verum
end;
A19: for x being set st x in [#] T1 holds
h . x = f . x
proof
let x be set ; ::_thesis: ( x in [#] T1 implies h . x = f . x )
assume A20: x in [#] T1 ; ::_thesis: h . x = f . x
now__::_thesis:_h_._x_=_f_._x
percases ( x in [#] T2 or not x in [#] T2 ) ;
supposeA21: x in [#] T2 ; ::_thesis: h . x = f . x
then  x in ([#] T1) /\ ([#] T2) by A20, XBOOLE_0:def_4;
then  x = p by A2, TARSKI:def_1;
hence  h . x = f . x by A8, A9, A21, FUNCT_4:13; ::_thesis: verum
end;
suppose not x in [#] T2 ; ::_thesis: h . x = f . x
hence  h . x = f . x by A9, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
hence  h . x = f . x ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_T1)_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_T1)_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )
thus  ( x in (h " P) /\ ([#] T1) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) )
proof
assume A22: x in (h " P) /\ ([#] T1) ; ::_thesis: x in f " P
then  x in h " P by XBOOLE_0:def_4;
then A23: h . x in P by FUNCT_1:def_7;
 f . x = h . x by A19, A22;
hence  x in f " P by A11, A22, A23, FUNCT_1:def_7; ::_thesis: verum
end;
assume A24: x in f " P ; ::_thesis: x in (h " P) /\ ([#] T1)
then  x in dom f by FUNCT_1:def_7;
then A25: x in dom h by A12, XBOOLE_0:def_3;
 f . x in P by A24, FUNCT_1:def_7;
then  h . x in P by A19, A24;
then  x in h " P by A25, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] T1) by A24, XBOOLE_0:def_4; ::_thesis: verum
end;
then A26: (h " P) /\ ([#] T1) = f " P by TARSKI:1;
assume A27: P is closed ; ::_thesis: h " P is closed
then  f " P is closed by A6, PRE_TOPC:def_6;
then  f " P is compact by A3, Th8;
then A28: P1 is compact by Th19;
 g " P is closed by A7, A27, PRE_TOPC:def_6;
then  g " P is compact by A4, Th8;
then A29: P2 is compact by Th19;
h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A11, A9, A12, RELAT_1:132, XBOOLE_1:28
.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;
then  h " P = (f " P) \/ (g " P) by A26, A13, TARSKI:1;
hence  h " P is closed by A5, A28, A29; ::_thesis: verum
end;
hence  f +* g is continuous Function of T,S by PRE_TOPC:def_6; ::_thesis: verum
end;

theorem :: COMPTS_1:21
for S, T being non empty TopSpace
for T1, T2 being SubSpace of T
for p1, p2 being Point of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
proof
let S, T be non empty TopSpace; ::_thesis: for T1, T2 being SubSpace of T
for p1, p2 being Point of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let T1, T2 be SubSpace of T; ::_thesis: for p1, p2 being Point of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let p1, p2 be Point of T; ::_thesis: for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let f be Function of T1,S; ::_thesis: for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let g be Function of T2,S; ::_thesis: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 implies f +* g is continuous Function of T,S )
assume that
A1: ([#] T1) \/ ([#] T2) = [#] T and
A2: ([#] T1) /\ ([#] T2) = {p1,p2} and
A3: T1 is compact and
A4: T2 is compact and
A5: T is T_2 and
A6: f is continuous and
A7: g is continuous and
A8: f . p1 = g . p1 and
A9: f . p2 = g . p2 ; ::_thesis: f +* g is continuous Function of T,S
set h = f +* g;
A10: dom g = [#] T2 by FUNCT_2:def_1;
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then A11: rng (f +* g) c= the carrier of S by XBOOLE_1:1;
A12: dom f = [#] T1 by FUNCT_2:def_1;
then  dom (f +* g) = the carrier of T by A1, A10, FUNCT_4:def_1;
then reconsider h = f +* g as Function of T,S by A11, FUNCT_2:def_1, RELSET_1:4;
 for P being Subset of S st P is closed holds
h " P is closed
proof
let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed )
 [#] T1 c= [#] T by A1, XBOOLE_1:7;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
 [#] T2 c= [#] T by A1, XBOOLE_1:7;
then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;
A13: dom h = (dom f) \/ (dom g) by FUNCT_4:def_1;
A14: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_T2)_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_T2)_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )
thus  ( x in (h " P) /\ ([#] T2) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) )
proof
assume A15: x in (h " P) /\ ([#] T2) ; ::_thesis: x in g " P
then  x in h " P by XBOOLE_0:def_4;
then A16: h . x in P by FUNCT_1:def_7;
 g . x = h . x by A10, A15, FUNCT_4:13;
hence  x in g " P by A10, A15, A16, FUNCT_1:def_7; ::_thesis: verum
end;
assume A17: x in g " P ; ::_thesis: x in (h " P) /\ ([#] T2)
then A18: x in dom g by FUNCT_1:def_7;
 g . x in P by A17, FUNCT_1:def_7;
then A19: h . x in P by A18, FUNCT_4:13;
 x in dom h by A13, A18, XBOOLE_0:def_3;
then  x in h " P by A19, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] T2) by A17, XBOOLE_0:def_4; ::_thesis: verum
end;
A20: for x being set st x in [#] T1 holds
h . x = f . x
proof
let x be set ; ::_thesis: ( x in [#] T1 implies h . x = f . x )
assume A21: x in [#] T1 ; ::_thesis: h . x = f . x
now__::_thesis:_h_._x_=_f_._x
percases ( x in [#] T2 or not x in [#] T2 ) ;
supposeA22: x in [#] T2 ; ::_thesis: h . x = f . x
then A23: x in ([#] T1) /\ ([#] T2) by A21, XBOOLE_0:def_4;
now__::_thesis:_h_._x_=_f_._x
percases ( x = p1 or x = p2 ) by A2, A23, TARSKI:def_2;
suppose x = p1 ; ::_thesis: h . x = f . x
hence  h . x = f . x by A8, A10, A22, FUNCT_4:13; ::_thesis: verum
end;
suppose x = p2 ; ::_thesis: h . x = f . x
hence  h . x = f . x by A9, A10, A22, FUNCT_4:13; ::_thesis: verum
end;
end;
end;
hence  h . x = f . x ; ::_thesis: verum
end;
suppose not x in [#] T2 ; ::_thesis: h . x = f . x
hence  h . x = f . x by A10, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
hence  h . x = f . x ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_T1)_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_T1)_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )
thus  ( x in (h " P) /\ ([#] T1) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) )
proof
assume A24: x in (h " P) /\ ([#] T1) ; ::_thesis: x in f " P
then  x in h " P by XBOOLE_0:def_4;
then A25: h . x in P by FUNCT_1:def_7;
 f . x = h . x by A20, A24;
hence  x in f " P by A12, A24, A25, FUNCT_1:def_7; ::_thesis: verum
end;
assume A26: x in f " P ; ::_thesis: x in (h " P) /\ ([#] T1)
then  x in dom f by FUNCT_1:def_7;
then A27: x in dom h by A13, XBOOLE_0:def_3;
 f . x in P by A26, FUNCT_1:def_7;
then  h . x in P by A20, A26;
then  x in h " P by A27, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] T1) by A26, XBOOLE_0:def_4; ::_thesis: verum
end;
then A28: (h " P) /\ ([#] T1) = f " P by TARSKI:1;
assume A29: P is closed ; ::_thesis: h " P is closed
then  f " P is closed by A6, PRE_TOPC:def_6;
then  f " P is compact by A3, Th8;
then A30: P1 is compact by Th19;
 g " P is closed by A7, A29, PRE_TOPC:def_6;
then  g " P is compact by A4, Th8;
then A31: P2 is compact by Th19;
h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A12, A10, A13, RELAT_1:132, XBOOLE_1:28
.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;
then  h " P = (f " P) \/ (g " P) by A28, A14, TARSKI:1;
hence  h " P is closed by A5, A30, A31; ::_thesis: verum
end;
hence  f +* g is continuous Function of T,S by PRE_TOPC:def_6; ::_thesis: verum
end;

begin

registration
let S be TopStruct ;
cluster the topology of S ->  open ;
coherence
 the topology of S is open
proof
let P be Subset of S; :: according to TOPS_2:def_1 ::_thesis: ( not P in the topology of S or P is open )
thus  ( not P in the topology of S or P is open ) by PRE_TOPC:def_2; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
cluster non empty open for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( b1 is open & not b1 is empty )
proof
take  the topology of T ; ::_thesis: ( the topology of T is open & not the topology of T is empty )
thus  ( the topology of T is open & not the topology of T is empty ) ; ::_thesis: verum
end;
end;

theorem Th22: :: COMPTS_1:22
for T being non empty TopSpace
for F being set holds
( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) )
proof
let T be non empty TopSpace; ::_thesis: for F being set holds
( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) )
let F be set ; ::_thesis: ( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) )
thus  ( F is open Subset-Family of T implies F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ) ::_thesis: ( F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) implies F is open Subset-Family of T )
proof
assume A1: F is open Subset-Family of T ; ::_thesis: F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #)
then reconsider F = F as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ;
 F is open
proof
let P be Subset of TopStruct(# the carrier of T, the topology of T #); :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
assume  P in F ; ::_thesis: P is open
then  P is open Subset of T by A1, TOPS_2:def_1;
hence  P is open by PRE_TOPC:30; ::_thesis: verum
end;
hence  F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: verum
end;
assume A2: F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: F is open Subset-Family of T
then reconsider F = F as Subset-Family of T ;
 F is open
proof
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
assume  P in F ; ::_thesis: P is open
then  P is open Subset of TopStruct(# the carrier of T, the topology of T #) by A2, TOPS_2:def_1;
hence  P is open by PRE_TOPC:30; ::_thesis: verum
end;
hence  F is open Subset-Family of T ; ::_thesis: verum
end;

theorem :: COMPTS_1:23
for T being non empty TopSpace
for X being set holds
( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) )
proof
let T be non empty TopSpace; ::_thesis: for X being set holds
( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; ::_thesis: ( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) )
thus  ( X is compact Subset of T implies X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ) ::_thesis: ( X is compact Subset of TopStruct(# the carrier of T, the topology of T #) implies X is compact Subset of T )
proof
assume A1: X is compact Subset of T ; ::_thesis: X is compact Subset of TopStruct(# the carrier of T, the topology of T #)
then reconsider Z = X as Subset of TopStruct(# the carrier of T, the topology of T #) ;
 Z is compact
proof
let F be Subset-Family of TopStruct(# the carrier of T, the topology of T #); :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st
( G c= F & G is Cover of Z & G is finite ) )
assume that
A2: F is Cover of Z and
A3: F is open ; ::_thesis: ex G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st
( G c= F & G is Cover of Z & G is finite )
reconsider FF = F as Subset-Family of T ;
 FF is open by A3, Th22;
then consider G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) such that
A4: G c= FF and
A5: G is Cover of X and
A6: G is finite by A1, A2, Def4;
take  G ; ::_thesis: ( G c= F & G is Cover of Z & G is finite )
thus  ( G c= F & G is Cover of Z & G is finite ) by A4, A5, A6; ::_thesis: verum
end;
hence  X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: verum
end;
assume A7: X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: X is compact Subset of T
then reconsider Z = X as Subset of T ;
 Z is compact
proof
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of Z & G is finite ) )
assume that
A8: F is Cover of Z and
A9: F is open ; ::_thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of Z & G is finite )
reconsider FF = F as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ;
 FF is open by A9, Th22;
then consider G being Subset-Family of T such that
A10: G c= FF and
A11: G is Cover of X and
A12: G is finite by A7, A8, Def4;
take  G ; ::_thesis: ( G c= F & G is Cover of Z & G is finite )
thus  ( G c= F & G is Cover of Z & G is finite ) by A10, A11, A12; ::_thesis: verum
end;
hence  X is compact Subset of T ; ::_thesis: verum
end;