set Y = One-Point_Compactification X;

set T = succ ([#] X);

set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;

A1: not [#] X in [#] X ;

A2: the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;

A3: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;

One-Point_Compactification X is TopSpace-like

set T = succ ([#] X);

set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;

A1: not [#] X in [#] X ;

A2: the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;

A3: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;

One-Point_Compactification X is TopSpace-like

proof

hence
One-Point_Compactification X is TopSpace-like
; :: thesis: verum
([#] X) ` =
(({} X) `) `

.= {} X ;

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

hence the carrier of (One-Point_Compactification X) in the topology of (One-Point_Compactification X) by A3, A2, XBOOLE_0:def 3; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b_{1} being Element of K19(K19( the carrier of (One-Point_Compactification X))) holds

( not b_{1} c= the topology of (One-Point_Compactification X) or union b_{1} in the topology of (One-Point_Compactification X) ) ) & ( for b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) holds

( not b_{1} in the topology of (One-Point_Compactification X) or not b_{2} in the topology of (One-Point_Compactification X) or b_{1} /\ b_{2} in the topology of (One-Point_Compactification X) ) ) )

assume A34: a in the topology of (One-Point_Compactification X) ; :: thesis: ( not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )

assume A35: b in the topology of (One-Point_Compactification X) ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

end;.= {} X ;

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

hence the carrier of (One-Point_Compactification X) in the topology of (One-Point_Compactification X) by A3, A2, XBOOLE_0:def 3; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b

( not b

( not b

hereby :: thesis: for b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) holds

( not b_{1} in the topology of (One-Point_Compactification X) or not b_{2} in the topology of (One-Point_Compactification X) or b_{1} /\ b_{2} in the topology of (One-Point_Compactification X) )

let a, b be Subset of (One-Point_Compactification X); :: thesis: ( not a in the topology of (One-Point_Compactification X) or not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )( not b

let a be Subset-Family of (One-Point_Compactification X); :: thesis: ( a c= the topology of (One-Point_Compactification X) implies union b_{1} in the topology of (One-Point_Compactification X) )

A4: not [#] X in [#] X ;

set ua = { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ;

A5: { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } c= the topology of X

union ua in the topology of X by A5, PRE_TOPC:def 1;

then A6: union ua is open ;

assume A7: a c= the topology of (One-Point_Compactification X) ; :: thesis: union b_{1} in the topology of (One-Point_Compactification X)

A8: union ua = (union a) \ {([#] X)}

end;A4: not [#] X in [#] X ;

set ua = { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ;

A5: { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } c= the topology of X

proof

then reconsider ua = { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } as Subset-Family of X by XBOOLE_1:1;
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 a or U \/ {([#] X)} in a ) ) } or x in the topology of X )

assume x in { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ; :: thesis: x in the topology of X

then ex U being Subset of X st

( x = U & U is open & ( U in a or U \/ {([#] X)} in a ) ) ;

hence x in the topology of X ; :: thesis: verum

end;assume x in { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ; :: thesis: x in the topology of X

then ex U being Subset of X st

( x = U & U is open & ( U in a or U \/ {([#] X)} in a ) ) ;

hence x in the topology of X ; :: thesis: verum

union ua in the topology of X by A5, PRE_TOPC:def 1;

then A6: union ua is open ;

assume A7: a c= the topology of (One-Point_Compactification X) ; :: thesis: union b

A8: union ua = (union a) \ {([#] X)}

proof

thus
union ua c= (union a) \ {([#] X)}
:: according to XBOOLE_0:def 10 :: thesis: (union a) \ {([#] X)} c= union ua

assume A16: x in (union a) \ {([#] X)} ; :: thesis: x in union ua

then x in union a by XBOOLE_0:def 5;

then consider A being set such that

A17: x in A and

A18: A in a by TARSKI:def 4;

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union a) \ {([#] X)} or x in union ua )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union ua or x in (union a) \ {([#] X)} )

assume x in union ua ; :: thesis: x in (union a) \ {([#] X)}

then consider A being set such that

A9: x in A and

A10: A in ua by TARSKI:def 4;

consider U being Subset of X such that

A11: A = U and

U is open and

A12: ( U in a or U \/ {([#] X)} in a ) by A10;

end;assume x in union ua ; :: thesis: x in (union a) \ {([#] X)}

then consider A being set such that

A9: x in A and

A10: A in ua by TARSKI:def 4;

consider U being Subset of X such that

A11: A = U and

U is open and

A12: ( U in a or U \/ {([#] X)} in a ) by A10;

A13: now :: thesis: x in union aend;

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

hence
x in (union a) \ {([#] X)}
by A13, XBOOLE_0:def 5; :: thesis: verumassume
x in {([#] X)}
; :: thesis: contradiction

then A15: x = [#] X by TARSKI:def 1;

A: x in [#] X by A9, A11;

reconsider xx = x as set by TARSKI:1;

not xx in xx ;

hence contradiction by A, A15; :: thesis: verum

end;then A15: x = [#] X by TARSKI:def 1;

A: x in [#] X by A9, A11;

reconsider xx = x as set by TARSKI:1;

not xx in xx ;

hence contradiction by A, A15; :: thesis: verum

assume A16: x in (union a) \ {([#] X)} ; :: thesis: x in union ua

then x in union a by XBOOLE_0:def 5;

then consider A being set such that

A17: x in A and

A18: A in a by TARSKI:def 4;

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

end;

suppose A19:
A in the topology of X
; :: thesis: x in union ua

then reconsider U = A as Subset of X ;

U is open by A19;

then U in ua by A18;

hence x in union ua by A17, TARSKI:def 4; :: thesis: verum

end;U is open by A19;

then U in ua by A18;

hence x in union ua by A17, TARSKI:def 4; :: thesis: verum

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

then consider U being Subset of X such that

A20: A = U \/ {([#] X)} and

A21: U is open and

U ` is compact ;

A22: U in ua by A18, A20, A21;

not x in {([#] X)} by A16, XBOOLE_0:def 5;

then x in U by A17, A20, XBOOLE_0:def 3;

hence x in union ua by A22, TARSKI:def 4; :: thesis: verum

end;A20: A = U \/ {([#] X)} and

A21: U is open and

U ` is compact ;

A22: U in ua by A18, A20, A21;

not x in {([#] X)} by A16, XBOOLE_0:def 5;

then x in U by A17, A20, XBOOLE_0:def 3;

hence x in union ua by A22, TARSKI:def 4; :: thesis: verum

per cases
( [#] X in union a or not [#] X in union a )
;

end;

suppose A23:
[#] X in union a
; :: thesis: union b_{1} in the topology of (One-Point_Compactification X)

then consider A being set such that

A24: [#] X in A and

A25: A in a by TARSKI:def 4;

( A in the topology of X or A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A2, A7, A25, XBOOLE_0:def 3;

then consider U being Subset of X such that

A26: A = U \/ {([#] X)} and

U is open and

A27: U ` is compact by A4, A24;

.= U by A28, ZFMISC_1:57 ;

then U c= union ua by A8, A25, XBOOLE_1:33, ZFMISC_1:74;

then A29: (union ua) ` is compact by A6, A27, COMPTS_1:9, XBOOLE_1:34;

(union ua) \/ {([#] X)} = (union a) \/ {([#] X)} by A8, XBOOLE_1:39

.= union a by A23, ZFMISC_1:40 ;

then union a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A6, A29;

hence union a in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

end;A24: [#] X in A and

A25: A in a by TARSKI:def 4;

( A in the topology of X or A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A2, A7, A25, XBOOLE_0:def 3;

then consider U being Subset of X such that

A26: A = U \/ {([#] X)} and

U is open and

A27: U ` is compact by A4, A24;

A28: now :: thesis: not [#] X in U

A \ {([#] X)} =
U \ {([#] X)}
by A26, XBOOLE_1:40
assume
[#] X in U
; :: thesis: contradiction

then [#] X in [#] X ;

hence contradiction ; :: thesis: verum

end;then [#] X in [#] X ;

hence contradiction ; :: thesis: verum

.= U by A28, ZFMISC_1:57 ;

then U c= union ua by A8, A25, XBOOLE_1:33, ZFMISC_1:74;

then A29: (union ua) ` is compact by A6, A27, COMPTS_1:9, XBOOLE_1:34;

(union ua) \/ {([#] X)} = (union a) \/ {([#] X)} by A8, XBOOLE_1:39

.= union a by A23, ZFMISC_1:40 ;

then union a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A6, A29;

hence union a in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

suppose A30:
not [#] X in union a
; :: thesis: union b_{1} in the topology of (One-Point_Compactification X)

A31:
a c= the topology of X

then union a in the topology of X by A31, PRE_TOPC:def 1;

hence union a in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

end;proof

then
a is Subset-Family of ([#] X)
by XBOOLE_1:1;
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in a or A in the topology of X )

reconsider AA = A as set by TARSKI:1;

assume A32: A in a ; :: thesis: A in the topology of X

assume not A in the topology of X ; :: thesis: contradiction

then A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A2, A7, A32, XBOOLE_0:def 3;

then A33: ex U being Subset of X st

( A = U \/ {([#] X)} & U is open & U ` is compact ) ;

[#] X in {([#] X)} by TARSKI:def 1;

then [#] X in AA by A33, XBOOLE_0:def 3;

hence contradiction by A30, A32, TARSKI:def 4; :: thesis: verum

end;reconsider AA = A as set by TARSKI:1;

assume A32: A in a ; :: thesis: A in the topology of X

assume not A in the topology of X ; :: thesis: contradiction

then A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A2, A7, A32, XBOOLE_0:def 3;

then A33: ex U being Subset of X st

( A = U \/ {([#] X)} & U is open & U ` is compact ) ;

[#] X in {([#] X)} by TARSKI:def 1;

then [#] X in AA by A33, XBOOLE_0:def 3;

hence contradiction by A30, A32, TARSKI:def 4; :: thesis: verum

then union a in the topology of X by A31, PRE_TOPC:def 1;

hence union a in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

assume A34: a in the topology of (One-Point_Compactification X) ; :: thesis: ( not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )

assume A35: b in the topology of (One-Point_Compactification X) ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

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

end;

suppose
( a in the topology of X & b in the topology of X )
; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

then
a /\ b in the topology of X
by PRE_TOPC:def 1;

hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

end;hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

suppose that A36:
a in the topology of X
and

A37: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

A37: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

reconsider a9 = a as Subset of X by A36;

not [#] X in a9 by A1;

then {([#] X)} misses a9 by ZFMISC_1:50;

then a9 /\ {([#] X)} = {} X ;

then reconsider aX = a9 /\ {([#] X)} as open Subset of X ;

consider U being Subset of X such that

A38: b = U \/ {([#] X)} and

A39: U is open and

U ` is compact by A37;

a9 is open by A36;

then reconsider aXU = a9 /\ U as open Subset of X by A39;

a /\ b = aXU \/ aX by A38, XBOOLE_1:23;

then a /\ b in the topology of X by PRE_TOPC:def 2;

hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

end;not [#] X in a9 by A1;

then {([#] X)} misses a9 by ZFMISC_1:50;

then a9 /\ {([#] X)} = {} X ;

then reconsider aX = a9 /\ {([#] X)} as open Subset of X ;

consider U being Subset of X such that

A38: b = U \/ {([#] X)} and

A39: U is open and

U ` is compact by A37;

a9 is open by A36;

then reconsider aXU = a9 /\ U as open Subset of X by A39;

a /\ b = aXU \/ aX by A38, XBOOLE_1:23;

then a /\ b in the topology of X by PRE_TOPC:def 2;

hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

suppose that A40:
b in the topology of X
and

A41: a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

A41: a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

reconsider b9 = b as Subset of X by A40;

not [#] X in b9 by A1;

then {([#] X)} misses b9 by ZFMISC_1:50;

then b9 /\ {([#] X)} = {} X ;

then reconsider bX = b9 /\ {([#] X)} as open Subset of X ;

consider U being Subset of X such that

A42: a = U \/ {([#] X)} and

A43: U is open and

U ` is compact by A41;

b9 is open by A40;

then reconsider bXUa = b9 /\ U as open Subset of X by A43;

a /\ b = bXUa \/ bX by A42, XBOOLE_1:23;

then a /\ b in the topology of X by PRE_TOPC:def 2;

hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

end;not [#] X in b9 by A1;

then {([#] X)} misses b9 by ZFMISC_1:50;

then b9 /\ {([#] X)} = {} X ;

then reconsider bX = b9 /\ {([#] X)} as open Subset of X ;

consider U being Subset of X such that

A42: a = U \/ {([#] X)} and

A43: U is open and

U ` is compact by A41;

b9 is open by A40;

then reconsider bXUa = b9 /\ U as open Subset of X by A43;

a /\ b = bXUa \/ bX by A42, XBOOLE_1:23;

then a /\ b in the topology of X by PRE_TOPC:def 2;

hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

suppose that A44:
a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) }
and

A45: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

A45: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)

consider Ua being Subset of X such that

A46: a = Ua \/ {([#] X)} and

A47: Ua is open and

A48: Ua ` is compact by A44;

consider Ub being Subset of X such that

A49: b = Ub \/ {([#] X)} and

A50: Ub is open and

A51: Ub ` is compact by A45;

(Ua `) \/ (Ub `) is compact by A48, A51, COMPTS_1:10;

then A52: (Ua /\ Ub) ` is compact by XBOOLE_1:54;

a /\ b = (Ua /\ Ub) \/ {([#] X)} by A46, A49, XBOOLE_1:24;

then a /\ b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A47, A50, A52;

hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum

end;A46: a = Ua \/ {([#] X)} and

A47: Ua is open and

A48: Ua ` is compact by A44;

consider Ub being Subset of X such that

A49: b = Ub \/ {([#] X)} and

A50: Ub is open and

A51: Ub ` is compact by A45;

(Ua `) \/ (Ub `) is compact by A48, A51, COMPTS_1:10;

then A52: (Ua /\ Ub) ` is compact by XBOOLE_1:54;

a /\ b = (Ua /\ Ub) \/ {([#] X)} by A46, A49, XBOOLE_1:24;

then a /\ b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A47, A50, A52;

hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum