:: TEX_2 semantic presentation

definition

let c₁ be non empty set ;
redefine attr a₁ is trivial means :Def1: :: TEX_2:def 1
ex b₁ being Element of a₁ st a₁ = {b₁};
compatibility

proof end;

end;

:: deftheorem Def1 defines trivial TEX_2:def 1 :

registration

cluster non empty trivial set ;
existence

proof end;

end;

theorem Th1: :: TEX_2:1

for b₁ being non empty set
for b₂ being non empty trivial set st b₁ c= b₂ holds
b₁ = b₂

proof end;

theorem Th2: :: TEX_2:2

for b₁ being non empty trivial set
for b₂ being set st not b₁ /\ b₂ is empty holds
b₁ c= b₂

proof end;

theorem Th3: :: TEX_2:3

canceled;

theorem Th4: :: TEX_2:4

for b₁, b₂ being 1-sorted st the carrier of b₁ = the carrier of b₂ & b₁ is trivial holds
b₂ is trivial

proof end;

definition

let c₁ be set ;
let c₂ be Element of c₁;
attr a₂ is proper means :Def2: :: TEX_2:def 2
a₂ <> union a₁;

end;

:: deftheorem Def2 defines proper TEX_2:def 2 :

registration

let c₁ be set ;
cluster non proper Element of K16(a₁);
existence

proof end;

end;

theorem Th5: :: TEX_2:5

for b₁ being set
for b₂ being Subset of b₁ holds
( b₂ is proper iff b₂ <> b₁ )

proof end;

registration

let c₁ be non empty set ;
cluster non proper -> non empty Element of K16(a₁);
coherence by Th5;
cluster empty -> proper Element of K16(a₁);
coherence by Th5;

end;

registration

let c₁ be non empty trivial set ;
cluster proper -> empty proper Element of K16(a₁);
coherence

proof end;

cluster non empty -> non empty non proper Element of K16(a₁);
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster proper Element of K16(a₁);
existence

proof end;

cluster non empty non proper Element of K16(a₁);
existence

proof end;

end;

registration

let c₁ be non empty set ;
cluster non empty trivial Element of K16(a₁);
existence

proof end;

end;

registration

let c₁ be set ;
cluster {a₁} -> trivial ;
coherence ;

end;

theorem Th6: :: TEX_2:6

for b₁ being non empty set
for b₂ being Element of b₁ st {b₂} is proper holds
not b₁ is trivial

proof end;

theorem Th7: :: TEX_2:7

for b₁ being non empty non trivial set
for b₂ being Element of b₁ holds {b₂} is proper by Th5;

registration

let c₁ be non empty trivial set ;
cluster non empty non proper -> non empty trivial non proper Element of K16(a₁);
coherence by Th5;

end;

registration

let c₁ be non empty non trivial set ;
cluster non empty trivial -> non empty proper Element of K16(a₁);
coherence by Th5;
cluster non empty non proper -> non empty non trivial Element of K16(a₁);
coherence by Th5;

end;

registration

let c₁ be non empty non trivial set ;
cluster non empty trivial proper Element of K16(a₁);
existence

proof end;

cluster non empty non trivial non proper Element of K16(a₁);
existence

proof end;

end;

theorem Th8: :: TEX_2:8

for b₁ being non empty 1-sorted
for b₂ being Element of b₁ st {b₂} is proper holds
not b₁ is trivial

proof end;

theorem Th9: :: TEX_2:9

for b₁ being non empty non trivial 1-sorted
for b₂ being Element of b₁ holds {b₂} is proper

proof end;

registration

let c₁ be non empty trivial 1-sorted ;
cluster non empty -> non empty non proper Element of K16(the carrier of a₁);
coherence

proof end;

cluster non empty non proper -> non empty trivial Element of K16(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be non empty non trivial 1-sorted ;
cluster non empty trivial -> non empty proper Element of K16(the carrier of a₁);
coherence

proof end;

cluster non empty non proper -> non empty non trivial Element of K16(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be non empty non trivial 1-sorted ;
cluster non empty trivial proper Element of K16(the carrier of a₁);
existence

proof end;

cluster non empty non trivial non proper Element of K16(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be non empty non trivial 1-sorted ;
cluster non empty trivial proper Element of K16(the carrier of a₁);
existence

proof end;

end;

theorem Th10: :: TEX_2:10

canceled;

theorem Th11: :: TEX_2:11

canceled;

theorem Th12: :: TEX_2:12

for b₁, b₂ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is TopSpace-like holds
b₂ is TopSpace-like

proof end;

definition

let c₁ be TopStruct ;
let c₂ be SubSpace of c₁;
attr a₂ is proper means :Def3: :: TEX_2:def 3
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is proper;

end;

:: deftheorem Def3 defines proper TEX_2:def 3 :

theorem Th13: :: TEX_2:13

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₃ is proper iff b₂ is proper )

proof end;

E10: now

let c₁ be TopStruct ;
let c₂ be SubSpace of c₁;
( [#] c₂ c= [#] c₁ & [#] c₂ = the carrier of c₂ ) by PRE_TOPC:def 9;
hence the carrier of c₂ is Subset of c₁ ;

end;

theorem Th14: :: TEX_2:14

for b₁ being TopStruct
for b₂, b₃ being SubSpace of b₁ st TopStruct(# the carrier of b₂,the topology of b₂ #) = TopStruct(# the carrier of b₃,the topology of b₃ #) & b₂ is proper holds
b₃ is proper

proof end;

theorem Th15: :: TEX_2:15

for b₁ being TopStruct
for b₂ being SubSpace of b₁ st the carrier of b₂ = the carrier of b₁ holds
not b₂ is proper

proof end;

registration

let c₁ be non empty trivial TopStruct ;
cluster non empty -> non empty non proper SubSpace of a₁;
coherence

proof end;

cluster non empty non proper -> non empty trivial SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty non trivial TopStruct ;
cluster non empty trivial -> non empty proper SubSpace of a₁;
coherence

proof end;

cluster non empty non proper -> non empty non trivial SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
cluster non empty strict non proper SubSpace of a₁;
existence

proof end;

end;

theorem Th16: :: TEX_2:16

for b₁ being non empty TopStruct
for b₂ being non proper SubSpace of b₁ holds TopStruct(# the carrier of b₂,the topology of b₂ #) = TopStruct(# the carrier of b₁,the topology of b₁ #)

proof end;

registration

let c₁ be non empty TopStruct ;
cluster discrete -> TopSpace-like SubSpace of a₁;
coherence

proof end;

cluster anti-discrete -> TopSpace-like SubSpace of a₁;
coherence

proof end;

cluster non TopSpace-like -> non discrete SubSpace of a₁;
coherence

proof end;

cluster non TopSpace-like -> non anti-discrete SubSpace of a₁;
coherence

proof end;

end;

theorem Th17: :: TEX_2:17

for b₁, b₂ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is discrete holds
b₂ is discrete

proof end;

theorem Th18: :: TEX_2:18

for b₁, b₂ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is anti-discrete holds
b₂ is anti-discrete

proof end;

registration

let c₁ be non empty TopStruct ;
cluster discrete -> almost_discrete SubSpace of a₁;
coherence

proof end;

cluster non almost_discrete -> non discrete SubSpace of a₁;
coherence

proof end;

cluster anti-discrete -> almost_discrete SubSpace of a₁;
coherence

proof end;

cluster non almost_discrete -> non anti-discrete SubSpace of a₁;
coherence

proof end;

end;

theorem Th19: :: TEX_2:19

for b₁, b₂ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is almost_discrete holds
b₂ is almost_discrete

proof end;

registration

let c₁ be non empty TopStruct ;
cluster non empty discrete anti-discrete -> non empty trivial SubSpace of a₁;
coherence

proof end;

cluster non empty anti-discrete non trivial -> non empty non discrete SubSpace of a₁;
coherence

proof end;

cluster non empty discrete non trivial -> non empty non anti-discrete SubSpace of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
func Sspace c₂ -> non empty strict SubSpace of a₁ means :Def4: :: TEX_2:def 4
the carrier of a₃ = {a₂};
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Sspace TEX_2:def 4 :

E15: now

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
set c₃ = Sspace c₂;
the carrier of (Sspace c₂) = {c₂} by Def4;
then reconsider c₄ = c₂ as Point of (Sspace c₂) by TARSKI:def 1;
the carrier of (Sspace c₂) = {c₄} by Def4;
hence Sspace c₂ is trivial by TEX_1:def 1;

end;

registration

let c₁ be non empty TopStruct ;
cluster non empty strict trivial SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
cluster Sspace a₂ -> non empty strict trivial ;
coherence by Lemma15;

end;

theorem Th20: :: TEX_2:20

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds
( Sspace b₂ is proper iff {b₂} is proper )

proof end;

theorem Th21: :: TEX_2:21

for b₁ being non empty TopStruct
for b₂ being Point of b₁ st Sspace b₂ is proper holds
not b₁ is trivial

proof end;

registration

let c₁ be non empty non trivial TopStruct ;
cluster non empty strict trivial proper SubSpace of a₁;
existence

proof end;

end;

theorem Th22: :: TEX_2:22

canceled;

theorem Th23: :: TEX_2:23

for b₁ being non empty TopStruct
for b₂ being non empty trivial SubSpace of b₁ ex b₃ being Point of b₁ st TopStruct(# the carrier of b₂,the topology of b₂ #) = TopStruct(# the carrier of (Sspace b₃),the topology of (Sspace b₃) #)

proof end;

theorem Th24: :: TEX_2:24

for b₁ being non empty TopStruct
for b₂ being Point of b₁ st Sspace b₂ is TopSpace-like holds
( Sspace b₂ is discrete & Sspace b₂ is anti-discrete )

proof end;

registration

let c₁ be non empty TopStruct ;
cluster non empty TopSpace-like trivial -> non empty TopSpace-like discrete anti-discrete almost_discrete trivial SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty strict TopSpace-like discrete anti-discrete almost_discrete trivial SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster Sspace a₂ -> non empty strict TopSpace-like discrete anti-discrete almost_discrete trivial ;
coherence ;

end;

registration

let c₁ be non empty TopSpace;
cluster non empty strict discrete anti-discrete almost_discrete trivial SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster Sspace a₂ -> non empty strict TopSpace-like discrete anti-discrete almost_discrete trivial ;
coherence ;

end;

registration

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

proof end;

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

proof end;

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

cluster non empty non trivial -> non empty non anti-discrete SubSpace of a₁;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

cluster non empty non trivial -> non empty non discrete SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty anti-discrete non trivial TopSpace;
cluster non empty proper -> non empty non open non closed proper SubSpace of a₁;
coherence

proof end;

cluster non empty discrete -> non empty discrete anti-discrete almost_discrete trivial proper SubSpace of a₁;
coherence ;

end;

registration

let c₁ be non empty anti-discrete non trivial TopSpace;
cluster strict non open non closed anti-discrete proper SubSpace of a₁;
existence

proof end;

end;

registration

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

proof end;

end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is discrete means :Def5: :: TEX_2:def 5
for b₁ being Subset of a₁ st b₁ c= a₂ holds
ex b₂ being Subset of a₁ st
( b₂ is open & a₂ /\ b₂ = b₁ );

end;

:: deftheorem Def5 defines discrete TEX_2:def 5 :

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
redefine attr a₂ is discrete means :Def6: :: TEX_2:def 6
for b₁ being Subset of a₁ st b₁ c= a₂ holds
ex b₂ being Subset of a₁ st
( b₂ is closed & a₂ /\ b₂ = b₁ );
compatibility

proof end;

end;

:: deftheorem Def6 defines discrete TEX_2:def 6 :

theorem Th25: :: TEX_2:25

for b₁, b₂ being TopStruct
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₄ & b₃ is discrete holds
b₄ is discrete

proof end;

theorem Th26: :: TEX_2:26

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

proof end;

theorem Th27: :: TEX_2:27

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ st b₂ = the carrier of b₁ holds
( b₂ is discrete iff b₁ is discrete )

proof end;

theorem Th28: :: TEX_2:28

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₃ c= b₂ & b₂ is discrete holds
b₃ is discrete

proof end;

theorem Th29: :: TEX_2:29

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st ( b₂ is discrete or b₃ is discrete ) holds
b₂ /\ b₃ is discrete

proof end;

theorem Th30: :: TEX_2:30

for b₁ being TopStruct st ( for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is open holds
( b₂ /\ b₃ is open & b₂ \/ b₃ is open ) ) holds
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is open & b₂ is discrete & b₃ is discrete holds
b₂ \/ b₃ is discrete

proof end;

theorem Th31: :: TEX_2:31

for b₁ being TopStruct st ( for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed holds
( b₂ /\ b₃ is closed & b₂ \/ b₃ is closed ) ) holds
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed & b₂ is discrete & b₃ is discrete holds
b₂ \/ b₃ is discrete

proof end;

theorem Th32: :: TEX_2:32

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is discrete holds
for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being Subset of b₁ st
( b₄ is open & b₂ /\ b₄ = {b₃} )

proof end;

theorem Th33: :: TEX_2:33

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ is discrete holds
for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being Subset of b₁ st
( b₄ is closed & b₂ /\ b₄ = {b₃} )

proof end;

theorem Th34: :: TEX_2:34

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

proof end;

theorem Th35: :: TEX_2:35

for b₁ being non empty TopSpace
for b₂ being empty Subset of b₁ holds b₂ is discrete

proof end;

theorem Th36: :: TEX_2:36

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds {b₂} is discrete

proof end;

theorem Th37: :: TEX_2:37

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st ( for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being Subset of b₁ st
( b₄ is open & b₂ /\ b₄ = {b₃} ) ) holds
b₂ is discrete

proof end;

theorem Th38: :: TEX_2:38

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is open & b₂ is discrete & b₃ is discrete holds
b₂ \/ b₃ is discrete

proof end;

theorem Th39: :: TEX_2:39

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed & b₂ is discrete & b₃ is discrete holds
b₂ \/ b₃ is discrete

proof end;

Lemma32: for b₁, b₂ being set st b₁ c= b₂ & b₁ <> b₂ holds
b₂ \ b₁ <> {}

proof end;

theorem Th40: :: TEX_2:40

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is everywhere_dense & b₂ is discrete holds
b₂ is open

proof end;

theorem Th41: :: TEX_2:41

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is discrete iff for b₃ being Subset of b₁ st b₃ c= b₂ holds
b₂ /\ (Cl b₃) = b₃ )

proof end;

theorem Th42: :: TEX_2:42

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is discrete holds
for b₃ being Point of b₁ st b₃ in b₂ holds
b₂ /\ (Cl {b₃}) = {b₃}

proof end;

theorem Th43: :: TEX_2:43

for b₁ being non empty discrete TopSpace
for b₂ being Subset of b₁ holds b₂ is discrete

proof end;

theorem Th44: :: TEX_2:44

for b₁ being non empty anti-discrete TopSpace
for b₂ being non empty Subset of b₁ holds
( b₂ is discrete iff b₂ is trivial )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is maximal_discrete means :Def7: :: TEX_2:def 7
( a₂ is discrete & ( for b₁ being Subset of a₁ st b₁ is discrete & a₂ c= b₁ holds
a₂ = b₁ ) );

end;

:: deftheorem Def7 defines maximal_discrete TEX_2:def 7 :

theorem Th45: :: TEX_2:45

proof end;

theorem Th46: :: TEX_2:46

for b₁ being non empty TopSpace
for b₂ being empty Subset of b₁ holds not b₂ is maximal_discrete

proof end;

theorem Th47: :: TEX_2:47

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is open & b₂ is maximal_discrete holds
b₂ is dense

proof end;

theorem Th48: :: TEX_2:48

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is dense & b₂ is discrete holds
b₂ is maximal_discrete

proof end;

theorem Th49: :: TEX_2:49

for b₁ being non empty discrete TopSpace
for b₂ being Subset of b₁ holds
( b₂ is maximal_discrete iff not b₂ is proper )

proof end;

theorem Th50: :: TEX_2:50

for b₁ being non empty anti-discrete TopSpace
for b₂ being non empty Subset of b₁ holds
( b₂ is maximal_discrete iff b₂ is trivial )

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be SubSpace of c₁;
attr a₂ is maximal_discrete means :Def8: :: TEX_2:def 8
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is maximal_discrete;

end;

:: deftheorem Def8 defines maximal_discrete TEX_2:def 8 :

theorem Th51: :: TEX_2:51

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

proof end;

registration

let c₁ be non empty TopStruct ;
cluster non empty maximal_discrete -> non empty TopSpace-like discrete almost_discrete SubSpace of a₁;
coherence

proof end;

cluster non empty non discrete -> non empty non maximal_discrete SubSpace of a₁;
coherence

proof end;

end;

theorem Th52: :: TEX_2:52

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

proof end;

theorem Th53: :: TEX_2:53

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

proof end;

registration

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

registration

let c₁ be non empty anti-discrete TopSpace;
cluster non empty maximal_discrete -> non empty discrete anti-discrete almost_discrete trivial SubSpace of a₁;
coherence

proof end;

cluster non empty non trivial -> non empty non maximal_discrete SubSpace of a₁;
coherence

proof end;

cluster non empty trivial -> non empty TopSpace-like discrete anti-discrete almost_discrete trivial maximal_discrete SubSpace of a₁;
coherence

proof end;

cluster non empty non maximal_discrete -> non empty non discrete non trivial non maximal_discrete SubSpace of a₁;
coherence

proof end;

end;

scheme :: TEX_2:sch 1
s1{ F₁() -> non empty TopStruct , F₂() -> Subset-Family of F₁(), P₁[ set , set ] } :

ex b₁ being Function of F₂(),the carrier of F₁() st
for b₂ being Subset of F₁() st b₂ in F₂() holds
P₁[b₂,b₁ . b₂]

provided

E44: for b₁ being Subset of F₁() st b₁ in F₂() holds
ex b₂ being Point of F₁() st P₁[b₁,b₂]

proof end;

theorem Th54: :: TEX_2:54

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ holds Cl b₂ = union { (Cl {b₃}) where B is Point of b₁ : b₃ in b₂ }

proof end;

theorem Th55: :: TEX_2:55

for b₁ being non empty almost_discrete TopSpace
for b₂, b₃ being Point of b₁ st b₂ in Cl {b₃} holds
Cl {b₂} = Cl {b₃}

proof end;

theorem Th56: :: TEX_2:56

for b₁ being non empty almost_discrete TopSpace
for b₂, b₃ being Point of b₁ holds
( Cl {b₂} misses Cl {b₃} or Cl {b₂} = Cl {b₃} )

proof end;

theorem Th57: :: TEX_2:57

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ st ( for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being Subset of b₁ st
( b₄ is closed & b₂ /\ b₄ = {b₃} ) ) holds
b₂ is discrete

proof end;

theorem Th58: :: TEX_2:58

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ st ( for b₃ being Point of b₁ st b₃ in b₂ holds
b₂ /\ (Cl {b₃}) = {b₃} ) holds
b₂ is discrete

proof end;

theorem Th59: :: TEX_2:59

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ holds
( b₂ is discrete iff for b₃, b₄ being Point of b₁ st b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ holds
Cl {b₃} misses Cl {b₄} )

proof end;

theorem Th60: :: TEX_2:60

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ holds
( b₂ is discrete iff for b₃ being Point of b₁ st b₃ in Cl b₂ holds
ex b₄ being Point of b₁ st
( b₄ in b₂ & b₂ /\ (Cl {b₃}) = {b₄} ) )

proof end;

theorem Th61: :: TEX_2:61

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ st ( b₂ is open or b₂ is closed ) & b₂ is maximal_discrete holds
not b₂ is proper

proof end;

theorem Th62: :: TEX_2:62

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ st b₂ is maximal_discrete holds
b₂ is dense

proof end;

theorem Th63: :: TEX_2:63

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ st b₂ is maximal_discrete holds
union { (Cl {b₃}) where B is Point of b₁ : b₃ in b₂ } = the carrier of b₁

proof end;

theorem Th64: :: TEX_2:64

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ holds
( b₂ is maximal_discrete iff for b₃ being Point of b₁ ex b₄ being Point of b₁ st
( b₄ in b₂ & b₂ /\ (Cl {b₃}) = {b₄} ) )

proof end;

theorem Th65: :: TEX_2:65

for b₁ being non empty almost_discrete TopSpace
for b₂ being Subset of b₁ st b₂ is discrete holds
ex b₃ being Subset of b₁ st
( b₂ c= b₃ & b₃ is maximal_discrete )

proof end;

theorem Th66: :: TEX_2:66

for b₁ being non empty almost_discrete TopSpace ex b₂ being Subset of b₁ st b₂ is maximal_discrete

proof end;

theorem Th67: :: TEX_2:67

for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty discrete SubSpace of b₁ ex b₃ being non empty strict SubSpace of b₁ st
( b₂ is SubSpace of b₃ & b₃ is maximal_discrete )

proof end;

registration

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

proof end;

cluster non empty non proper -> non empty non maximal_discrete SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty non anti-discrete almost_discrete TopSpace;
cluster non empty maximal_discrete -> non empty non trivial SubSpace of a₁;
coherence

proof end;

cluster non empty trivial -> non empty non maximal_discrete SubSpace of a₁;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th68: :: TEX_2:68

for b₁ being discrete TopSpace
for b₂ being TopSpace
for b₃ being Function of b₁,b₂ holds b₃ is continuous

proof end;

theorem Th69: :: TEX_2:69

for b₁ being non empty TopSpace st ( for b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ holds b₃ is continuous ) holds
b₁ is discrete

proof end;

theorem Th70: :: TEX_2:70

for b₁ being non empty TopSpace
for b₂ being non empty anti-discrete TopSpace
for b₃ being Function of b₁,b₂ holds b₃ is continuous

proof end;

theorem Th71: :: TEX_2:71

for b₁ being non empty TopSpace st ( for b₂ being non empty TopSpace
for b₃ being Function of b₂,b₁ holds b₃ is continuous ) holds
b₁ is anti-discrete

proof end;

theorem Th72: :: TEX_2:72

for b₁ being non empty discrete TopSpace
for b₂ being non empty SubSpace of b₁ ex b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction

proof end;

theorem Th73: :: TEX_2:73

for b₁ being non empty discrete TopSpace
for b₂ being non empty SubSpace of b₁ holds b₂ is_a_retract_of b₁

proof end;

theorem Th74: :: TEX_2:74

for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty maximal_discrete SubSpace of b₁ ex b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction

proof end;

theorem Th75: :: TEX_2:75

for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty maximal_discrete SubSpace of b₁ holds b₂ is_a_retract_of b₁

proof end;

Lemma59: for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty maximal_discrete SubSpace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Point of b₂
for b₅ being Point of b₁ st b₄ = b₅ holds
Cl {b₅} c= b₃ " {b₄}

proof end;

theorem Th76: :: TEX_2:76

for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty maximal_discrete SubSpace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Subset of b₂
for b₅ being Subset of b₁ st b₄ = b₅ holds
b₃ " b₄ = Cl b₅

proof end;

theorem Th77: :: TEX_2:77

for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty maximal_discrete SubSpace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Point of b₂
for b₅ being Point of b₁ st b₄ = b₅ holds
b₃ " {b₄} = Cl {b₅} by Th76;

theorem Th78: :: TEX_2:78

for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty discrete SubSpace of b₁ ex b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction

proof end;

theorem Th79: :: TEX_2:79

for b₁ being non empty almost_discrete TopSpace
for b₂ being non empty discrete SubSpace of b₁ holds b₂ is_a_retract_of b₁

proof end;