let F be Subset-Family of (One-Point_Compactification X); :: according to COMPTS_1:def 3 :: thesis:
assume that
A1: F is Cover of (One-Point_Compactification X) and
A2: F is open ; :: thesis:
A3: not [#] X in [#] X ;
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A4: [#] (One-Point_Compactification X) c= union F by A1, SETFAM_1:def 12;
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 set ; :: according to TARSKI:def 3 :: thesis:
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:
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 by PRE_TOPC:def 5; :: thesis:

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;
[#] 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 A4, TARSKI:def 4;
reconsider A = A as Subset of (One-Point_Compactification X) by A6;
A is open by A2, A6, TOPS_2:def 1;
then A in the topology of (One-Point_Compactification X) by PRE_TOPC:def 5;
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 A in the topology of X by A3, 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 ;
A10: Fx is open

proof

let P be Subset of X; :: according to TOPS_2:def 1 :: thesis:
assume P in Fx ; :: thesis:
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:

end;

Fx is Cover of X

proof

let x be set ; :: according to TARSKI:def 3,SETFAM_1:def 12 :: thesis:
assume A11: x in the carrier of X ; :: thesis:
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
A12: x in B and
A13: B in F by TARSKI:def 4, A4;
reconsider B = B as Subset of (One-Point_Compactification X) by A13;
B is open by A2, A13, TOPS_2:def 1;
then B in the topology of (One-Point_Compactification X) by PRE_TOPC:def 5;
then A14: B in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;

per cases by A14, XBOOLE_0:def 3;

suppose A15: B in the topology of X ; :: thesis:

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

end;

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

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

now

assume x in {([#] X)} ; :: thesis:
then x = [#] X by TARSKI:def 1;
hence contradiction by A11; :: thesis:

end;

then A18: x in Bx by A12, A16, XBOOLE_0:def 3;
Bx in Fx by A13, A16, A17;
hence x in union Fx by A18, TARSKI:def 4; :: thesis:

end;

then [#] X = union Fx by SETFAM_1:60;
then Fx is Cover of U ` by SETFAM_1:def 12;
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, A10, COMPTS_1:def 7;
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)} ) ) ) ) } ;
defpred S₁[ set , set ] means ( X in Gx & ( X \/ {([#] X)} in F implies c₂ = X \/ {([#] X)} ) & ( not X \/ {([#] X)} in F implies c₂ = X ) );
A22: for x being set st x in Gx holds
ex y being set 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 set ; :: thesis:
assume A23: x in Gx ; :: thesis:
then x in Fx by A19;
then consider U being Subset of X such that
A24: x = U and
U is open and
A25: ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ;

per cases ;

suppose A26: not U \/ {([#] X)} in F ; :: thesis:

then reconsider y = U as Subset of (One-Point_Compactification X) by A25;
take y ; :: thesis:
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 A23, A24, A25, A26; :: thesis:
thus S₁[x,y] by A23, A24, A26; :: thesis:

end;

suppose A27: U \/ {([#] X)} in F ; :: thesis:

then reconsider y = U \/ {([#] X)} as Subset of (One-Point_Compactification X) ;
take y ; :: thesis:
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 A23, A24, A27; :: thesis:
thus S₁[x,y] by A23, A24, A27; :: thesis:

end;

consider f being Function such that
A28: 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
A29: for x being set st x in Gx holds
S₁[x,f . x] from WELLORD2:sch 1(A22);
A30: { 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 set ; :: according to TARSKI:def 3 :: thesis:
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:
then consider W being Subset of (One-Point_Compactification X) such that
A31: y = W and
W in F and
A32: 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
A33: V in Gx and
A34: ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) by A32;
f . V in rng f by A28, A33, FUNCT_1:12;
hence y in rng f by A29, A31, A33, A34; :: thesis:

end;

A35: rng f is finite by A21, A28, FINSET_1:26;
{ 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 set ; :: according to TARSKI:def 3 :: thesis:
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:
then consider W being Subset of (One-Point_Compactification X) such that
A36: x = W and
A37: 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, A37, TOPS_2:def 1;
hence x in the topology of (One-Point_Compactification X) by A36, PRE_TOPC:def 5; :: thesis:

end;

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 A30, A35, XBOOLE_1:1;
take G = GX \/ {A}; :: thesis:
A38: GX c= F

proof

let P be set ; :: according to TARSKI:def 3 :: thesis:
assume P in GX ; :: thesis:
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:

end;

{A} c= F by A6, ZFMISC_1:37;
hence G c= F by A38, XBOOLE_1:8; :: thesis:
union G = [#] (One-Point_Compactification X)

proof

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

per cases by A39, XBOOLE_0:def 3;

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

then P in (U ` ) \/ U by PRE_TOPC:18;
then A40: ( P in U ` or P in U ) by XBOOLE_0:def 3;
U ` c= union Gx by A20, SETFAM_1:def 12;
then A41: ( P in union Gx or P in U ) by A40;
union Gx c= union GX

proof

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

per cases by A45;

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

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

end;

suppose A46: Z \/ {([#] X)} in F ; :: thesis:

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

end;

then ( P in union GX or P in A ) by A8, A41, XBOOLE_0:def 3;
then ( P in union GX or P in union {A} ) by ZFMISC_1:31;
then P in (union GX) \/ (union {A}) by XBOOLE_0:def 3;
hence P in union G by ZFMISC_1:96; :: thesis:

end;

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

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

end;

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