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


begin

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 )
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;

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
proofend;

begin

:: 2. Dense and Everywhere Dense Subspaces.
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT 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 )
proofend;

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
proofend;
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 )
proofend;
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
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT 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 )
proofend;

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
proofend;
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
proofend;
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 )
proofend;
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
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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
proofend;
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 )
proofend;
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
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

begin

:: 3. Boundary and Nowhere Dense Subspaces.
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT 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 )
proofend;

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
proofend;
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
proofend;
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 )
proofend;

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 )
proofend;

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
proofend;

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
proofend;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT 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 )
proofend;

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
proofend;
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
proofend;
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 )
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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
proofend;
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 )
proofend;

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 ) )
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

begin

:: 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
proofend;

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
proofend;

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 )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

begin

:: 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
proofend;

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
proofend;

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
proofend;
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
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;
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 )
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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 #) ) )
proofend;

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 #) ) )
proofend;

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 )
proofend;

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 )
proofend;