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 = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
A3: [#] = succ ([#] X) by Def9;
One-Point_Compactification X is TopSpace-like
proof
([#] 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 in the topology of by ; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of K19(K19( the carrier of )) holds
( not b1 c= the topology of or union b1 in the topology of ) ) & ( for b1, b2 being Element of K19( the carrier of ) holds
( not b1 in the topology of or not b2 in the topology of or b1 /\ b2 in the topology of ) ) )

hereby :: thesis: for b1, b2 being Element of K19( the carrier of ) holds
( not b1 in the topology of or not b2 in the topology of or b1 /\ b2 in the topology of )
let a be Subset-Family of ; :: thesis: ( a c= the topology of implies union b1 in the topology of )
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
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;
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;
union ua in the topology of X by ;
then A6: union ua is open ;
assume A7: a c= the topology of ; :: thesis: union b1 in the topology of
A8: union ua = () \ {([#] X)}
proof
thus union ua c= () \ {([#] X)} :: according to XBOOLE_0:def 10 :: thesis: () \ {([#] X)} c= union ua
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union ua or x in () \ {([#] X)} )
assume x in union ua ; :: thesis: x in () \ {([#] 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 a
per cases ( U in a or U \/ {([#] X)} in a ) by A12;
end;
end;
now :: thesis: not x in {([#] X)}
assume x in {([#] X)} ; :: thesis: contradiction
then A15: x = [#] X by TARSKI:def 1;
A: x in [#] X by ;
reconsider xx = x as set by TARSKI:1;
not xx in xx ;
hence contradiction by A, A15; :: thesis: verum
end;
hence x in () \ {([#] X)} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () \ {([#] X)} or x in union ua )
assume A16: x in () \ {([#] 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 ;
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 ; :: thesis: verum
end;
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 ;
not x in {([#] X)} by ;
then x in U by ;
hence x in union ua by ; :: thesis: verum
end;
end;
end;
per cases ( [#] X in union a or not [#] X in union a ) ;
suppose A23: [#] X in union a ; :: thesis: union b1 in the topology of
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 ;
then consider U being Subset of X such that
A26: A = U \/ {([#] X)} and
U is open and
A27: U ` is compact by ;
A28: now :: thesis: not [#] X in U
assume [#] X in U ; :: thesis: contradiction
then [#] X in [#] X ;
hence contradiction ; :: thesis: verum
end;
A \ {([#] X)} = U \ {([#] X)} by
.= U by ;
then U c= union ua by ;
then A29: (union ua) ` is compact by ;
(union ua) \/ {([#] X)} = () \/ {([#] X)} by
.= union a by ;
then union a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by ;
hence union a in the topology of by ; :: thesis: verum
end;
suppose A30: not [#] X in union a ; :: thesis: union b1 in the topology of
A31: a c= the topology of X
proof
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 ;
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 ;
hence contradiction by A30, A32, TARSKI:def 4; :: thesis: verum
end;
then a is Subset-Family of ([#] X) by XBOOLE_1:1;
then union a in the topology of X by ;
hence union a in the topology of by ; :: thesis: verum
end;
end;
end;
let a, b be Subset of ; :: thesis: ( not a in the topology of or not b in the topology of or a /\ b in the topology of )
assume A34: a in the topology of ; :: thesis: ( not b in the topology of or a /\ b in the topology of )
assume A35: b in the topology of ; :: thesis: a /\ b in the topology of
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 ;
suppose ( a in the topology of X & b in the topology of X ) ; :: thesis: a /\ b in the topology of
then a /\ b in the topology of X by PRE_TOPC:def 1;
hence a /\ b in the topology of by ; :: thesis: verum
end;
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
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 ;
then a /\ b in the topology of X by PRE_TOPC:def 2;
hence a /\ b in the topology of by ; :: thesis: verum
end;
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
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 ;
then a /\ b in the topology of X by PRE_TOPC:def 2;
hence a /\ b in the topology of by ; :: thesis: verum
end;
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
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 ;
then A52: (Ua /\ Ub) ` is compact by XBOOLE_1:54;
a /\ b = (Ua /\ Ub) \/ {([#] X)} by ;
then a /\ b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by ;
hence a /\ b in the topology of by ; :: thesis: verum
end;
end;
end;
hence One-Point_Compactification X is TopSpace-like ; :: thesis: verum