set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
let F be Subset-Family of (One-Point_Compactification X); :: according to COMPTS_1:def 1 :: thesis: ( not F is Cover of the carrier of (One-Point_Compactification X) or not F is open or ex b₁ being Element of K19(K19( the carrier of (One-Point_Compactification X))) st
( b₁ c= F & b₁ is Cover of the carrier of (One-Point_Compactification X) & b₁ is finite ) )
assume that
A1: F is Cover of (One-Point_Compactification X) and
A2: F is open ; :: thesis: ex b₁ being Element of K19(K19( the carrier of (One-Point_Compactification X))) st
( b₁ c= F & b₁ is Cover of the carrier of (One-Point_Compactification X) & b₁ is finite )
A3: [#] (One-Point_Compactification X) c= union F by A1, SETFAM_1:def 11;
set Fx = { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } ;
{ U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } c= the topology of X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } or x in the topology of X )
assume x in { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } ; :: thesis: x in the topology of X
then ex U being Subset of X st
( x = U & U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) ;
hence x in the topology of X ; :: thesis: verum

end;

then reconsider Fx = { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } as Subset-Family of X by XBOOLE_1:1;
A4: Fx is open

proof

let P be Subset of X; :: according to TOPS_2:def 1 :: thesis: ( not P in Fx or P is open )
assume P in Fx ; :: thesis: P is open
then ex U being Subset of X st
( P = U & U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) ;
hence P is open ; :: thesis: verum

end;

[#] X in {([#] X)} by TARSKI:def 1;
then [#] X in succ ([#] X) by XBOOLE_0:def 3;
then [#] X in [#] (One-Point_Compactification X) by Def9;
then consider A being set such that
A5: [#] X in A and
A6: A in F by A3, TARSKI:def 4;
reconsider A = A as Subset of (One-Point_Compactification X) by A6;
A is open by A2, A6;
then A in the topology of (One-Point_Compactification X) ;
then A7: A in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
not [#] X in [#] X ;
then not A in the topology of X by A5;
then A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A7, XBOOLE_0:def 3;
then consider U being Subset of X such that
A8: A = U \/ {([#] X)} and
U is open and
A9: U ` is compact ;
Fx is Cover of X

proof

let x be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not x in the carrier of X or x in union Fx )
assume A10: x in the carrier of X ; :: thesis: x in union Fx
then x in succ ([#] X) by XBOOLE_0:def 3;
then x in [#] (One-Point_Compactification X) by Def9;
then consider B being set such that
A11: x in B and
A12: B in F by A3, TARSKI:def 4;
reconsider B = B as Subset of (One-Point_Compactification X) by A12;
B is open by A2, A12;
then B in the topology of (One-Point_Compactification X) ;
then A13: B in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;

per cases ( B in the topology of X or B in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A13, XBOOLE_0:def 3;

suppose A14: B in the topology of X ; :: thesis: x in union Fx

then reconsider Bx = B as Subset of X ;
A15: ( ( Bx in F & not Bx \/ {([#] X)} in F ) or Bx \/ {([#] X)} in F ) by A12;
Bx is open by A14;
then Bx in Fx by A15;
hence x in union Fx by A11, TARSKI:def 4; :: thesis: verum

end;

suppose B in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: x in union Fx

then consider Bx being Subset of X such that
A16: B = Bx \/ {([#] X)} and
A17: Bx is open and
Bx ` is compact ;
A18: Bx in Fx by A12, A16, A17;

now :: thesis: not x in {([#] X)}

assume x in {([#] X)} ; :: thesis: contradiction
then A: x = [#] X by TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx ;
hence contradiction by A, A10; :: thesis: verum

end;

then x in Bx by A11, A16, XBOOLE_0:def 3;
hence x in union Fx by A18, TARSKI:def 4; :: thesis: verum

end;

end;

end;

then [#] X = union Fx by SETFAM_1:45;
then Fx is Cover of U ` by SETFAM_1:def 11;
then consider Gx being Subset-Family of X such that
A19: Gx c= Fx and
A20: Gx is Cover of U ` and
A21: Gx is finite by A9, A4;
set GX = { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } ;
A22: { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } c= the topology of (One-Point_Compactification X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } or x in the topology of (One-Point_Compactification X) )
assume x in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } ; :: thesis: x in the topology of (One-Point_Compactification X)
then consider W being Subset of (One-Point_Compactification X) such that
A23: x = W and
A24: W in F and
ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ;
W is open by A2, A24;
hence x in the topology of (One-Point_Compactification X) by A23; :: thesis: verum

end;

defpred S₁[ object , object ] means ex D1 being set st
( D1 = X & X in Gx & ( D1 \/ {([#] X)} in F implies c₂ = D1 \/ {([#] X)} ) & ( not D1 \/ {([#] X)} in F implies c₂ = X ) );
A25: for x being object st x in Gx holds
ex y being object st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Gx implies ex y being object st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S₁[x,y] ) )
assume A26: x in Gx ; :: thesis: ex y being object st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S₁[x,y] )
then x in Fx by A19;
then consider U being Subset of X such that
A27: x = U and
U is open and
A28: ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ;

per cases ( not U \/ {([#] X)} in F or U \/ {([#] X)} in F ) ;

suppose A29: not U \/ {([#] X)} in F ; :: thesis: ex y being object st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S₁[x,y] )

then reconsider y = U as Subset of (One-Point_Compactification X) by A28;
reconsider y = y as object ;
take y ; :: thesis: ( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S₁[x,y] )
thus y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } by A26, A27, A28, A29; :: thesis: S₁[x,y]
thus S₁[x,y] by A26, A27, A29; :: thesis: verum

end;

suppose A30: U \/ {([#] X)} in F ; :: thesis: ex y being object st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S₁[x,y] )

then reconsider y = U \/ {([#] X)} as Subset of (One-Point_Compactification X) ;
take y ; :: thesis: ( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S₁[x,y] )
thus y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } by A26, A27, A30; :: thesis: S₁[x,y]
thus S₁[x,y] by A26, A27, A30; :: thesis: verum

end;

end;

end;

consider f being Function such that
A31: dom f = Gx and
rng f c= { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } and
A32: for x being object st x in Gx holds
S₁[x,f . x] from FUNCT_1:sch 6(A25);
A33: { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } c= rng f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } or y in rng f )
assume y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } ; :: thesis: y in rng f
then consider W being Subset of (One-Point_Compactification X) such that
A34: y = W and
W in F and
A35: ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ;
consider V being Subset of X such that
A36: V in Gx and
A37: ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) by A35;
A38: f . V in rng f by A31, A36, FUNCT_1:3;
S₁[V,f . V] by A32, A36;
hence y in rng f by A34, A37, A38; :: thesis: verum

end;

rng f is finite by A21, A31, FINSET_1:8;
then reconsider GX = { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } as finite Subset-Family of (One-Point_Compactification X) by A33, A22, XBOOLE_1:1;
take G = GX \/ {A}; :: thesis: ( G c= F & G is Cover of the carrier of (One-Point_Compactification X) & G is finite )
A39: GX c= F

proof

let P be object ; :: according to TARSKI:def 3 :: thesis: ( not P in GX or P in F )
assume P in GX ; :: thesis: P in F
then ex W being Subset of (One-Point_Compactification X) st
( P = W & W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) ;
hence P in F ; :: thesis: verum

end;

{A} c= F by A6, ZFMISC_1:31;
hence G c= F by A39, XBOOLE_1:8; :: thesis: ( G is Cover of the carrier of (One-Point_Compactification X) & G is finite )
union G = [#] (One-Point_Compactification X)

proof

thus union G c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def 10 :: thesis: [#] (One-Point_Compactification X) c= union G
let P be object ; :: according to TARSKI:def 3 :: thesis: ( not P in [#] (One-Point_Compactification X) or P in union G )
assume P in [#] (One-Point_Compactification X) ; :: thesis: P in union G
then A40: P in succ ([#] X) by Def9;

per cases ( P in [#] X or P in {([#] X)} ) by A40, XBOOLE_0:def 3;

suppose P in [#] X ; :: thesis: P in union G

then P in (U `) \/ U by PRE_TOPC:2;
then A41: ( P in U ` or P in U ) by XBOOLE_0:def 3;
A42: union Gx c= union GX

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union Gx or z in union GX )
assume z in union Gx ; :: thesis: z in union GX
then consider S being set such that
A43: z in S and
A44: S in Gx by TARSKI:def 4;
S in Fx by A19, A44;
then consider Z being Subset of X such that
A45: S = Z and
Z is open and
A46: ( ( Z in F & not Z \/ {([#] X)} in F ) or Z \/ {([#] X)} in F ) ;

per cases ( ( Z in F & not Z \/ {([#] X)} in F ) or Z \/ {([#] X)} in F ) by A46;

suppose ( Z in F & not Z \/ {([#] X)} in F ) ; :: thesis: z in union GX

then Z in GX by A44, A45;
hence z in union GX by A43, A45, TARSKI:def 4; :: thesis: verum

end;

suppose A47: Z \/ {([#] X)} in F ; :: thesis: z in union GX

A48: z in Z \/ {([#] X)} by A43, A45, XBOOLE_0:def 3;
Z \/ {([#] X)} in GX by A44, A45, A47;
hence z in union GX by A48, TARSKI:def 4; :: thesis: verum

end;

end;

end;

U ` c= union Gx by A20, SETFAM_1:def 11;
then ( P in union Gx or P in U ) by A41;
then ( P in union GX or P in A ) by A8, A42, XBOOLE_0:def 3;
then ( P in union GX or P in union {A} ) by ZFMISC_1:25;
then P in (union GX) \/ (union {A}) by XBOOLE_0:def 3;
hence P in union G by ZFMISC_1:78; :: thesis: verum

end;

suppose A49: P in {([#] X)} ; :: thesis: P in union G

A in {A} by TARSKI:def 1;
then A50: A in G by XBOOLE_0:def 3;
P = [#] X by A49, TARSKI:def 1;
hence P in union G by A5, A50, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence G is Cover of (One-Point_Compactification X) by SETFAM_1:def 11; :: thesis: G is finite
thus G is finite ; :: thesis: verum