:: On Nowhere and Everywhere Dense Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received November 9, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users


theorem Th1: :: TEX_3:1
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )
proof end;

Lm1: for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B

proof end;

Lm2: for X being non empty TopSpace
for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B

proof end;

theorem Th2: :: TEX_3:2
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is dense iff B is boundary )
proof end;

theorem :: TEX_3:3
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is boundary iff B is dense ) by Th2;

theorem Th4: :: TEX_3:4
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is everywhere_dense iff B is nowhere_dense )
proof end;

theorem :: TEX_3:5
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is nowhere_dense iff B is everywhere_dense ) by Th4;

theorem Th6: :: TEX_3:6
for X being non empty TopSpace
for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )
proof end;

theorem :: TEX_3:7
for X being non trivial TopSpace
for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
proof end;

theorem Th8: :: TEX_3:8
for X being non trivial TopSpace
for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
proof end;

:: 2. Dense and Everywhere Dense Subspaces.
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is dense means :Def1: :: TEX_3:def 1
for A being Subset of X st A = the carrier of IT holds
A is dense ;
end;

:: deftheorem Def1 defines dense TEX_3:def 1 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is dense iff for A being Subset of X st A = the carrier of IT holds
A is dense );

theorem Th9: :: TEX_3:9
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense ) ;

registration
let X be non empty TopSpace;
cluster closed dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is closed holds
not b1 is proper
proof end;
cluster proper dense -> non closed for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is closed
;
cluster closed proper -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper & b1 is closed holds
not b1 is dense
;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is strict & not b1 is empty )
proof end;
end;

::Properties of Dense Subspaces.
theorem Th10: :: TEX_3:10
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is dense holds
ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:11
for X being non empty TopSpace
for X0 being non empty dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
proof end;

theorem :: TEX_3:12
for X being non empty TopSpace
for X1 being dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
proof end;

theorem :: TEX_3:13
for X being non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
proof end;

theorem :: TEX_3:14
for X being non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
proof end;

theorem :: TEX_3:15
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )
proof end;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is everywhere_dense means :Def2: :: TEX_3:def 2
for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense ;
end;

:: deftheorem Def2 defines everywhere_dense TEX_3:def 2 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is everywhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense );

theorem Th16: :: TEX_3:16
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense ) ;

registration
let X be non empty TopSpace;
cluster everywhere_dense -> dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
b1 is dense
by TOPS_3:33;
cluster non dense -> non everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is dense holds
not b1 is everywhere_dense
;
cluster non proper -> everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is proper holds
b1 is everywhere_dense
proof end;
cluster non everywhere_dense -> proper for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is everywhere_dense holds
b1 is proper
;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like everywhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is strict & not b1 is empty )
proof end;
end;

::Properties of Everywhere Dense Subspaces.
theorem Th17: :: TEX_3:17
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is everywhere_dense holds
ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:18
for X being non empty TopSpace
for X0 being non empty everywhere_dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
proof end;

theorem :: TEX_3:19
for X being non empty TopSpace
for X1 being everywhere_dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
proof end;

theorem :: TEX_3:20
for X being non empty TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
proof end;

theorem :: TEX_3:21
for X being non empty TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
proof end;

theorem :: TEX_3:22
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )
proof end;

registration
let X be non empty TopSpace;
cluster open dense -> everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is open holds
b1 is everywhere_dense
proof end;
cluster dense non everywhere_dense -> non open for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & not b1 is everywhere_dense holds
not b1 is open
;
cluster open non everywhere_dense -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & not b1 is everywhere_dense holds
not b1 is dense
;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like open dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is strict & not b1 is empty )
proof end;
end;

::Properties of Dense Open Subspaces.
theorem Th23: :: TEX_3:23
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is dense & A0 is open holds
ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:24
for X being non empty TopSpace
for X0 being SubSpace of X holds
( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
proof end;

theorem :: TEX_3:25
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds
X1 union X2 is dense SubSpace of X
proof end;

theorem :: TEX_3:26
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds
X1 union X2 is everywhere_dense SubSpace of X
proof end;

theorem :: TEX_3:27
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds
X1 meet X2 is everywhere_dense SubSpace of X
proof end;

theorem :: TEX_3:28
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds
X1 meet X2 is dense SubSpace of X
proof end;

:: 3. Boundary and Nowhere Dense Subspaces.
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is boundary means :Def3: :: TEX_3:def 3
for A being Subset of X st A = the carrier of IT holds
A is boundary ;
end;

:: deftheorem Def3 defines boundary TEX_3:def 3 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is boundary iff for A being Subset of X st A = the carrier of IT holds
A is boundary );

theorem Th29: :: TEX_3:29
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary ) ;

registration
let X be non empty TopSpace;
cluster non empty open -> non empty non boundary for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is open holds
not b1 is boundary
proof end;
cluster non empty boundary -> non empty non open for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is open
;
cluster everywhere_dense -> non boundary for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is boundary
proof end;
cluster boundary -> non everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary holds
not b1 is everywhere_dense
;
end;

::Properties of Boundary Subspaces.
theorem Th30: :: TEX_3:30
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof end;

theorem Th31: :: TEX_3:31
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is dense iff X2 is boundary )
proof end;

theorem :: TEX_3:32
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is boundary iff X2 is dense ) by Th31;

theorem Th33: :: TEX_3:33
for X being non empty TopSpace
for X0 being SubSpace of X st X0 is boundary holds
for A being Subset of X st A c= the carrier of X0 holds
A is boundary
proof end;

theorem Th34: :: TEX_3:34
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1 is boundary & X2 is SubSpace of X1 holds
X2 is boundary by TSEP_1:4, Th33;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attr IT is nowhere_dense means :Def4: :: TEX_3:def 4
for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense ;
end;

:: deftheorem Def4 defines nowhere_dense TEX_3:def 4 :
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is nowhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense );

theorem Th35: :: TEX_3:35
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense ) ;

registration
let X be non empty TopSpace;
cluster nowhere_dense -> boundary for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is nowhere_dense holds
b1 is boundary
proof end;
cluster non boundary -> non nowhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is boundary holds
not b1 is nowhere_dense
;
cluster nowhere_dense -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is nowhere_dense holds
not b1 is dense
proof end;
cluster dense -> non nowhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense holds
not b1 is nowhere_dense
;
end;

::Properties of Nowhere Dense Subspaces.
theorem :: TEX_3:36
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 )
proof end;

theorem Th37: :: TEX_3:37
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is everywhere_dense iff X2 is nowhere_dense )
proof end;

theorem :: TEX_3:38
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is nowhere_dense iff X2 is everywhere_dense ) by Th37;

theorem Th39: :: TEX_3:39
for X being non empty TopSpace
for X0 being SubSpace of X st X0 is nowhere_dense holds
for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
proof end;

theorem Th40: :: TEX_3:40
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds
X2 is nowhere_dense by TSEP_1:4, Th39;

registration
let X be non empty TopSpace;
cluster closed boundary -> nowhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary & b1 is closed holds
b1 is nowhere_dense
proof end;
cluster boundary non nowhere_dense -> non closed for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary & not b1 is nowhere_dense holds
not b1 is closed
;
cluster closed non nowhere_dense -> non boundary for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is closed & not b1 is nowhere_dense holds
not b1 is boundary
;
end;

::Properties of Boundary Closed Subspaces.
theorem Th41: :: TEX_3:41
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof end;

theorem :: TEX_3:42
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
proof end;

theorem :: TEX_3:43
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds
X1 meet X2 is boundary
proof end;

theorem :: TEX_3:44
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds
X1 union X2 is nowhere_dense
proof end;

theorem :: TEX_3:45
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds
X1 union X2 is boundary
proof end;

theorem :: TEX_3:46
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds
X1 meet X2 is nowhere_dense
proof end;

:: 4. Dense and Boundary Subspaces of non Discrete Spaces.
theorem :: TEX_3:47
for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is boundary ) holds
X is discrete
proof end;

theorem :: TEX_3:48
for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is dense ) holds
X is discrete
proof end;

registration
let X be non empty discrete TopSpace;
cluster non empty -> non empty non boundary for SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds not b1 is boundary
;
cluster proper -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is dense
;
cluster dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense holds
not b1 is proper
;
end;

registration
let X be non empty discrete TopSpace;
cluster non empty strict TopSpace-like closed open discrete almost_discrete non boundary for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is boundary & b1 is strict & not b1 is empty )
proof end;
end;

registration
let X be non trivial discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete non dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is dense & b1 is strict )
proof end;
end;

theorem :: TEX_3:49
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is boundary holds
not X is discrete ;

theorem :: TEX_3:50
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is proper ) holds
not X is discrete ;

registration
let X be non empty non discrete TopSpace;
cluster non empty strict TopSpace-like boundary for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is boundary & b1 is strict & not b1 is empty )
proof end;
cluster non empty strict TopSpace-like proper dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

theorem :: TEX_3:51
for X being non empty non discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:52
for X being non empty non discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense holds
ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:53
for X being non empty non discrete TopSpace
for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:54
for X being non empty non discrete TopSpace
for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:55
for X being non empty non discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )
proof end;

:: 5. Everywhere and Nowhere Dense Subspaces of non Almost Discrete Spaces.
theorem :: TEX_3:56
for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) holds
X is almost_discrete
proof end;

theorem :: TEX_3:57
for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) holds
X is almost_discrete
proof end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty -> non empty non nowhere_dense for SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds not b1 is nowhere_dense
proof end;
cluster proper -> non everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is everywhere_dense
proof end;
cluster everywhere_dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is proper
;
cluster non empty boundary -> non empty non closed for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is closed
;
cluster non empty closed -> non empty non boundary for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is closed holds
not b1 is boundary
;
cluster proper dense -> non open for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is open
;
cluster open dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is open holds
not b1 is proper
;
cluster open proper -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & b1 is proper holds
not b1 is dense
;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict TopSpace-like non nowhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof end;
end;

registration
let X be non trivial almost_discrete TopSpace;
cluster strict TopSpace-like non everywhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is everywhere_dense & b1 is strict )
proof end;
end;

theorem :: TEX_3:58
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is nowhere_dense holds
not X is almost_discrete ;

theorem :: TEX_3:59
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is boundary & X0 is closed ) holds
not X is almost_discrete ;

theorem :: TEX_3:60
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is everywhere_dense & X0 is proper ) holds
not X is almost_discrete ;

theorem :: TEX_3:61
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is open & X0 is proper ) holds
not X is almost_discrete ;

registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict TopSpace-like nowhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof end;
cluster non empty strict TopSpace-like proper everywhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th62: :: TEX_3:62
for X being non empty non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:63
for X being non empty non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is everywhere_dense holds
ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:64
for X being non empty non almost_discrete TopSpace
for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:65
for X being non empty non almost_discrete TopSpace
for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:66
for X being non empty non almost_discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )
proof end;

registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict TopSpace-like closed boundary for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is boundary & b1 is closed & b1 is strict & not b1 is empty )
proof end;
cluster non empty strict TopSpace-like open proper dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is proper & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th67: :: TEX_3:67
for X being non empty non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:68
for X being non empty non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds
ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
proof end;

theorem :: TEX_3:69
for X being non empty non almost_discrete TopSpace
for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:70
for X being non empty non almost_discrete TopSpace
for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof end;

theorem :: TEX_3:71
for X being non empty non almost_discrete TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
proof end;

theorem :: TEX_3:72
for X being non empty non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
proof end;

theorem :: TEX_3:73
for X being non empty non almost_discrete TopSpace
for X0 being non empty everywhere_dense SubSpace of X holds
( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
proof end;

theorem :: TEX_3:74
for X being non empty non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
proof end;

theorem :: TEX_3:75
for X being non empty non almost_discrete TopSpace
for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
proof end;