:: TEX_3 semantic presentation

theorem Th1: :: TEX_3:1

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( not b₂ is empty iff b₃ is proper )

proof end;

Lemma2: for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is everywhere_dense & b₃ is everywhere_dense holds
b₂ meets b₃

proof end;

Lemma3: for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st ( ( b₂ is everywhere_dense & b₃ is dense ) or ( b₂ is dense & b₃ is everywhere_dense ) ) holds
b₂ meets b₃

proof end;

theorem Th2: :: TEX_3:2

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is dense iff b₃ is boundary )

proof end;

theorem Th3: :: TEX_3:3

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is boundary iff b₃ is dense ) by Th2;

theorem Th4: :: TEX_3:4

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is everywhere_dense iff b₃ is nowhere_dense )

proof end;

theorem Th5: :: TEX_3:5

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is nowhere_dense iff b₃ is everywhere_dense ) by Th4;

theorem Th6: :: TEX_3:6

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is proper & b₃ is proper )

proof end;

theorem Th7: :: TEX_3:7

for b₁ being non empty non trivial TopSpace
for b₂ being non empty proper Subset of b₁ ex b₃ being non empty strict proper SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th8: :: TEX_3:8

for b₁ being non empty non trivial TopSpace
for b₂ being non empty proper SubSpace of b₁ ex b₃ being non empty strict proper SubSpace of b₁ st b₂,b₃ constitute_a_decomposition

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be SubSpace of c₁;
attr a₂ is dense means :Def1: :: TEX_3:def 1
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is dense;

end;

:: deftheorem Def1 defines dense TEX_3:def 1 :

theorem Th9: :: TEX_3:9

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₂ is dense iff b₃ is dense )

proof end;

registration

let c₁ be non empty TopSpace;
cluster closed dense -> non proper SubSpace of a₁;
coherence

proof end;

cluster proper dense -> non closed SubSpace of a₁;
coherence

proof end;

cluster closed proper -> non dense SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty strict dense SubSpace of a₁;
existence

proof end;

end;

theorem Th10: :: TEX_3:10

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is dense holds
ex b₃ being non empty strict dense SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th11: :: TEX_3:11

for b₁ being non empty TopSpace
for b₂ being non empty dense SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
( b₄ is dense iff b₃ is dense )

proof end;

theorem Th12: :: TEX_3:12

for b₁ being non empty TopSpace
for b₂ being dense SubSpace of b₁
for b₃ being SubSpace of b₁ st b₂ is SubSpace of b₃ holds
b₃ is dense

proof end;

theorem Th13: :: TEX_3:13

for b₁ being non empty TopSpace
for b₂ being non empty dense SubSpace of b₁
for b₃ being non empty SubSpace of b₁ st b₂ is SubSpace of b₃ holds
b₂ is dense SubSpace of b₃

proof end;

theorem Th14: :: TEX_3:14

for b₁ being non empty TopSpace
for b₂ being non empty dense SubSpace of b₁
for b₃ being non empty dense SubSpace of b₂ holds b₃ is non empty dense SubSpace of b₁

proof end;

theorem Th15: :: TEX_3:15

for b₁, b₂, b₃ being non empty TopSpace st b₃ = TopStruct(# the carrier of b₂,the topology of b₂ #) holds
( b₂ is dense SubSpace of b₁ iff b₃ is dense SubSpace of b₁ )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be SubSpace of c₁;
attr a₂ is everywhere_dense means :Def2: :: TEX_3:def 2
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is everywhere_dense;

end;

:: deftheorem Def2 defines everywhere_dense TEX_3:def 2 :

theorem Th16: :: TEX_3:16

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₂ is everywhere_dense iff b₃ is everywhere_dense )

proof end;

registration

let c₁ be non empty TopSpace;
cluster everywhere_dense -> dense SubSpace of a₁;
coherence

proof end;

cluster non dense -> non everywhere_dense SubSpace of a₁;
coherence

proof end;

cluster non proper -> everywhere_dense SubSpace of a₁;
coherence

proof end;

cluster non everywhere_dense -> proper SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty strict dense everywhere_dense SubSpace of a₁;
existence

proof end;

end;

theorem Th17: :: TEX_3:17

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is everywhere_dense holds
ex b₃ being non empty strict everywhere_dense SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th18: :: TEX_3:18

for b₁ being non empty TopSpace
for b₂ being non empty everywhere_dense SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
( b₄ is everywhere_dense iff b₃ is everywhere_dense )

proof end;

theorem Th19: :: TEX_3:19

for b₁ being non empty TopSpace
for b₂ being everywhere_dense SubSpace of b₁
for b₃ being SubSpace of b₁ st b₂ is SubSpace of b₃ holds
b₃ is everywhere_dense

proof end;

theorem Th20: :: TEX_3:20

for b₁ being non empty TopSpace
for b₂ being non empty everywhere_dense SubSpace of b₁
for b₃ being non empty SubSpace of b₁ st b₂ is SubSpace of b₃ holds
b₂ is everywhere_dense SubSpace of b₃

proof end;

theorem Th21: :: TEX_3:21

for b₁ being non empty TopSpace
for b₂ being non empty everywhere_dense SubSpace of b₁
for b₃ being non empty everywhere_dense SubSpace of b₂ holds b₃ is everywhere_dense SubSpace of b₁

proof end;

theorem Th22: :: TEX_3:22

for b₁, b₂, b₃ being non empty TopSpace st b₃ = TopStruct(# the carrier of b₂,the topology of b₂ #) holds
( b₂ is everywhere_dense SubSpace of b₁ iff b₃ is everywhere_dense SubSpace of b₁ )

proof end;

registration

let c₁ be non empty TopSpace;
cluster open dense -> dense everywhere_dense SubSpace of a₁;
coherence

proof end;

cluster dense non everywhere_dense -> non open SubSpace of a₁;
coherence

proof end;

cluster open non everywhere_dense -> proper non dense non everywhere_dense SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty strict open dense everywhere_dense SubSpace of a₁;
existence

proof end;

end;

theorem Th23: :: TEX_3:23

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is dense & b₂ is open holds
ex b₃ being non empty strict open dense SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th24: :: TEX_3:24

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁ holds
( b₂ is everywhere_dense iff ex b₃ being strict open dense SubSpace of b₁ st b₃ is SubSpace of b₂ )

proof end;

theorem Th25: :: TEX_3:25

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st ( b₂ is dense or b₃ is dense ) holds
b₂ union b₃ is dense SubSpace of b₁

proof end;

theorem Th26: :: TEX_3:26

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st ( b₂ is everywhere_dense or b₃ is everywhere_dense ) holds
b₂ union b₃ is everywhere_dense SubSpace of b₁

proof end;

theorem Th27: :: TEX_3:27

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ is everywhere_dense & b₃ is everywhere_dense holds
b₂ meet b₃ is everywhere_dense SubSpace of b₁

proof end;

theorem Th28: :: TEX_3:28

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st ( ( b₂ is everywhere_dense & b₃ is dense ) or ( b₂ is dense & b₃ is everywhere_dense ) ) holds
b₂ meet b₃ is dense SubSpace of b₁

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be SubSpace of c₁;
attr a₂ is boundary means :Def3: :: TEX_3:def 3
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is boundary;

end;

:: deftheorem Def3 defines boundary TEX_3:def 3 :

theorem Th29: :: TEX_3:29

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₂ is boundary iff b₃ is boundary )

proof end;

registration

let c₁ be non empty TopSpace;
cluster non empty open -> non empty non boundary SubSpace of a₁;
coherence

proof end;

cluster non empty boundary -> non empty non open SubSpace of a₁;
coherence

proof end;

cluster everywhere_dense -> non boundary SubSpace of a₁;
coherence

proof end;

cluster boundary -> proper non everywhere_dense SubSpace of a₁;
coherence

proof end;

end;

theorem Th30: :: TEX_3:30

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is boundary holds
ex b₃ being strict SubSpace of b₁ st
( b₃ is boundary & b₂ = the carrier of b₃ )

proof end;

theorem Th31: :: TEX_3:31

for b₁ being non empty TopSpace
for b₂, b₃ being SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is dense iff b₃ is boundary )

proof end;

theorem Th32: :: TEX_3:32

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is boundary iff b₃ is dense ) by Th31;

theorem Th33: :: TEX_3:33

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁ st b₂ is boundary holds
for b₃ being Subset of b₁ st b₃ c= the carrier of b₂ holds
b₃ is boundary

proof end;

theorem Th34: :: TEX_3:34

for b₁ being non empty TopSpace
for b₂, b₃ being SubSpace of b₁ st b₂ is boundary & b₃ is SubSpace of b₂ holds
b₃ is boundary

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be SubSpace of c₁;
attr a₂ is nowhere_dense means :Def4: :: TEX_3:def 4
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is nowhere_dense;

end;

:: deftheorem Def4 defines nowhere_dense TEX_3:def 4 :

theorem Th35: :: TEX_3:35

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₂ is nowhere_dense iff b₃ is nowhere_dense )

proof end;

registration

let c₁ be non empty TopSpace;
cluster nowhere_dense -> proper non everywhere_dense boundary SubSpace of a₁;
coherence

proof end;

cluster non boundary -> non nowhere_dense SubSpace of a₁;
coherence

proof end;

cluster nowhere_dense -> proper non dense non everywhere_dense SubSpace of a₁;
coherence

proof end;

cluster dense -> non nowhere_dense SubSpace of a₁;
coherence

proof end;

end;

theorem Th36: :: TEX_3:36

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is nowhere_dense holds
ex b₃ being strict SubSpace of b₁ st
( b₃ is nowhere_dense & b₂ = the carrier of b₃ )

proof end;

theorem Th37: :: TEX_3:37

for b₁ being non empty TopSpace
for b₂, b₃ being SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is everywhere_dense iff b₃ is nowhere_dense )

proof end;

theorem Th38: :: TEX_3:38

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is nowhere_dense iff b₃ is everywhere_dense ) by Th37;

theorem Th39: :: TEX_3:39

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁ st b₂ is nowhere_dense holds
for b₃ being Subset of b₁ st b₃ c= the carrier of b₂ holds
b₃ is nowhere_dense

proof end;

theorem Th40: :: TEX_3:40

for b₁ being non empty TopSpace
for b₂, b₃ being SubSpace of b₁ st b₂ is nowhere_dense & b₃ is SubSpace of b₂ holds
b₃ is nowhere_dense

proof end;

registration

let c₁ be non empty TopSpace;
cluster closed boundary -> proper non dense non everywhere_dense boundary nowhere_dense SubSpace of a₁;
coherence

proof end;

cluster boundary non nowhere_dense -> non closed SubSpace of a₁;
coherence

proof end;

cluster closed non nowhere_dense -> non boundary non nowhere_dense SubSpace of a₁;
coherence

proof end;

end;

theorem Th41: :: TEX_3:41

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is boundary & b₂ is closed holds
ex b₃ being non empty strict closed SubSpace of b₁ st
( b₃ is boundary & b₂ = the carrier of b₃ )

proof end;

theorem Th42: :: TEX_3:42

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ holds
( b₂ is nowhere_dense iff ex b₃ being non empty strict closed SubSpace of b₁ st
( b₃ is boundary & b₂ is SubSpace of b₃ ) )

proof end;

theorem Th43: :: TEX_3:43

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st ( b₂ is boundary or b₃ is boundary ) & b₂ meets b₃ holds
b₂ meet b₃ is boundary

proof end;

theorem Th44: :: TEX_3:44

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂ is nowhere_dense & b₃ is nowhere_dense holds
b₂ union b₃ is nowhere_dense

proof end;

theorem Th45: :: TEX_3:45

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st ( ( b₂ is nowhere_dense & b₃ is boundary ) or ( b₂ is boundary & b₃ is nowhere_dense ) ) holds
b₂ union b₃ is boundary

proof end;

theorem Th46: :: TEX_3:46

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st ( b₂ is nowhere_dense or b₃ is nowhere_dense ) & b₂ meets b₃ holds
b₂ meet b₃ is nowhere_dense

proof end;

theorem Th47: :: TEX_3:47

for b₁ being non empty TopSpace st ( for b₂ being SubSpace of b₁ holds not b₂ is boundary ) holds
b₁ is discrete

proof end;

theorem Th48: :: TEX_3:48

for b₁ being non empty non trivial TopSpace st ( for b₂ being proper SubSpace of b₁ holds not b₂ is dense ) holds
b₁ is discrete

proof end;

registration

let c₁ be non empty discrete TopSpace;
cluster non empty -> non empty non boundary non nowhere_dense SubSpace of a₁;
coherence ;
cluster proper -> proper non dense non everywhere_dense SubSpace of a₁;
coherence

proof end;

cluster dense -> non proper dense everywhere_dense non boundary non nowhere_dense SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty discrete TopSpace;
cluster non empty strict non boundary non nowhere_dense SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty discrete non trivial TopSpace;
cluster strict proper non dense non everywhere_dense SubSpace of a₁;
existence

proof end;

end;

theorem Th49: :: TEX_3:49

for b₁ being non empty TopSpace st ex b₂ being non empty SubSpace of b₁ st b₂ is boundary holds
not b₁ is discrete

proof end;

theorem Th50: :: TEX_3:50

for b₁ being non empty TopSpace st ex b₂ being non empty SubSpace of b₁ st
( b₂ is dense & b₂ is proper ) holds
not b₁ is discrete

proof end;

registration

let c₁ be non empty non discrete TopSpace;
cluster non empty strict non open proper non everywhere_dense boundary SubSpace of a₁;
existence

proof end;

cluster non empty strict non closed proper dense non nowhere_dense SubSpace of a₁;
existence

proof end;

end;

theorem Th51: :: TEX_3:51

for b₁ being non empty non discrete TopSpace
for b₂ being non empty Subset of b₁ st b₂ is boundary holds
ex b₃ being strict boundary SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th52: :: TEX_3:52

for b₁ being non empty non discrete TopSpace
for b₂ being non empty proper Subset of b₁ st b₂ is dense holds
ex b₃ being strict proper dense SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th53: :: TEX_3:53

for b₁ being non empty non discrete TopSpace
for b₂ being non empty boundary SubSpace of b₁ ex b₃ being non empty strict proper dense SubSpace of b₁ st b₂,b₃ constitute_a_decomposition

proof end;

theorem Th54: :: TEX_3:54

for b₁ being non empty non discrete TopSpace
for b₂ being non empty proper dense SubSpace of b₁ ex b₃ being non empty strict boundary SubSpace of b₁ st b₂,b₃ constitute_a_decomposition

proof end;

theorem Th55: :: TEX_3:55

for b₁ being non empty non discrete TopSpace
for b₂, b₃ being non empty TopSpace st b₃ = TopStruct(# the carrier of b₂,the topology of b₂ #) holds
( b₂ is boundary SubSpace of b₁ iff b₃ is boundary SubSpace of b₁ )

proof end;

theorem Th56: :: TEX_3:56

for b₁ being non empty TopSpace st ( for b₂ being SubSpace of b₁ holds not b₂ is nowhere_dense ) holds
b₁ is almost_discrete

proof end;

theorem Th57: :: TEX_3:57

for b₁ being non empty non trivial TopSpace st ( for b₂ being proper SubSpace of b₁ holds not b₂ is everywhere_dense ) holds
b₁ is almost_discrete

proof end;

registration

let c₁ be non empty almost_discrete TopSpace;
cluster non empty -> non empty non nowhere_dense SubSpace of a₁;
coherence

proof end;

cluster proper -> proper non everywhere_dense SubSpace of a₁;
coherence

proof end;

cluster everywhere_dense -> non proper dense everywhere_dense non boundary non nowhere_dense SubSpace of a₁;
coherence

proof end;

cluster non empty boundary -> non empty non closed SubSpace of a₁;
coherence

proof end;

cluster non empty closed -> non empty non boundary non nowhere_dense SubSpace of a₁;
coherence

proof end;

cluster proper dense -> non open SubSpace of a₁;
coherence

proof end;

cluster open dense -> non proper dense everywhere_dense non boundary non nowhere_dense SubSpace of a₁;
coherence

proof end;

cluster open proper -> proper non dense non everywhere_dense SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty almost_discrete TopSpace;
cluster non empty strict non nowhere_dense SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty almost_discrete non trivial TopSpace;
cluster strict proper non everywhere_dense SubSpace of a₁;
existence

proof end;

end;

theorem Th58: :: TEX_3:58

for b₁ being non empty TopSpace st ex b₂ being non empty SubSpace of b₁ st b₂ is nowhere_dense holds
not b₁ is almost_discrete

proof end;

theorem Th59: :: TEX_3:59

for b₁ being non empty TopSpace st ex b₂ being non empty SubSpace of b₁ st
( b₂ is boundary & b₂ is closed ) holds
not b₁ is almost_discrete

proof end;

theorem Th60: :: TEX_3:60

for b₁ being non empty TopSpace st ex b₂ being non empty SubSpace of b₁ st
( b₂ is everywhere_dense & b₂ is proper ) holds
not b₁ is almost_discrete

proof end;

theorem Th61: :: TEX_3:61

for b₁ being non empty TopSpace st ex b₂ being non empty SubSpace of b₁ st
( b₂ is dense & b₂ is open & b₂ is proper ) holds
not b₁ is almost_discrete

proof end;

registration

let c₁ be non empty non almost_discrete TopSpace;
cluster non empty strict non open proper non dense non everywhere_dense boundary nowhere_dense SubSpace of a₁;
existence

proof end;

cluster non empty strict non closed proper dense everywhere_dense non boundary non nowhere_dense SubSpace of a₁;
existence

proof end;

end;

theorem Th62: :: TEX_3:62

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty Subset of b₁ st b₂ is nowhere_dense holds
ex b₃ being non empty strict nowhere_dense SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th63: :: TEX_3:63

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty proper Subset of b₁ st b₂ is everywhere_dense holds
ex b₃ being strict proper everywhere_dense SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th64: :: TEX_3:64

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty nowhere_dense SubSpace of b₁ ex b₃ being non empty strict proper everywhere_dense SubSpace of b₁ st b₂,b₃ constitute_a_decomposition

proof end;

theorem Th65: :: TEX_3:65

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty proper everywhere_dense SubSpace of b₁ ex b₃ being non empty strict nowhere_dense SubSpace of b₁ st b₂,b₃ constitute_a_decomposition

proof end;

theorem Th66: :: TEX_3:66

for b₁ being non empty non almost_discrete TopSpace
for b₂, b₃ being non empty TopSpace st b₃ = TopStruct(# the carrier of b₂,the topology of b₂ #) holds
( b₂ is nowhere_dense SubSpace of b₁ iff b₃ is nowhere_dense SubSpace of b₁ )

proof end;

registration

let c₁ be non empty non almost_discrete TopSpace;
cluster non empty strict closed non open proper non dense non everywhere_dense boundary nowhere_dense SubSpace of a₁;
existence

proof end;

cluster non empty strict non closed open proper dense everywhere_dense non boundary non nowhere_dense SubSpace of a₁;
existence

proof end;

end;

theorem Th67: :: TEX_3:67

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty Subset of b₁ st b₂ is boundary & b₂ is closed holds
ex b₃ being non empty strict closed boundary SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th68: :: TEX_3:68

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty proper Subset of b₁ st b₂ is dense & b₂ is open holds
ex b₃ being strict open proper dense SubSpace of b₁ st b₂ = the carrier of b₃

proof end;

theorem Th69: :: TEX_3:69

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty closed boundary SubSpace of b₁ ex b₃ being non empty strict open proper dense SubSpace of b₁ st b₂,b₃ constitute_a_decomposition

proof end;

theorem Th70: :: TEX_3:70

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty open proper dense SubSpace of b₁ ex b₃ being non empty strict closed boundary SubSpace of b₁ st b₂,b₃ constitute_a_decomposition

proof end;

theorem Th71: :: TEX_3:71

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty SubSpace of b₁ holds
( b₂ is nowhere_dense iff ex b₃ being non empty strict closed boundary SubSpace of b₁ st b₂ is SubSpace of b₃ )

proof end;

theorem Th72: :: TEX_3:72

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty nowhere_dense SubSpace of b₁ holds
( ( b₂ is boundary & b₂ is closed ) or ex b₃ being non empty strict proper everywhere_dense SubSpace of b₁ex b₄ being non empty strict closed boundary SubSpace of b₁ st
( b₃ meet b₄ = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ union b₄ = TopStruct(# the carrier of b₁,the topology of b₁ #) ) )

proof end;

theorem Th73: :: TEX_3:73

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty everywhere_dense SubSpace of b₁ holds
( ( b₂ is dense & b₂ is open ) or ex b₃ being non empty strict open proper dense SubSpace of b₁ex b₄ being non empty strict nowhere_dense SubSpace of b₁ st
( b₃ misses b₄ & b₃ union b₄ = TopStruct(# the carrier of b₂,the topology of b₂ #) ) )

proof end;

theorem Th74: :: TEX_3:74

for b₁ being non empty non almost_discrete TopSpace
for b₂ being non empty nowhere_dense SubSpace of b₁ ex b₃ being non empty strict open proper dense SubSpace of b₁ex b₄ being non empty strict closed boundary SubSpace of b₁ st
( b₃,b₄ constitute_a_decomposition & b₂ is SubSpace of b₄ )

proof end;

theorem Th75: :: TEX_3:75

for b₁ being non empty non almost_discrete TopSpace
for b₂ being proper everywhere_dense SubSpace of b₁ ex b₃ being strict open proper dense SubSpace of b₁ex b₄ being strict closed boundary SubSpace of b₁ st
( b₃,b₄ constitute_a_decomposition & b₃ is SubSpace of b₂ )

proof end;