:: TEX_2 semantic presentation

definition

let X be non empty set ;
redefine attr X is trivial means :Def1: :: TEX_2:def 1
ex s being Element of X st X = {s};
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 A being non empty set
for B being non empty trivial set st A c= B holds
A = B

proof end;

theorem :: TEX_2:2

for A being non empty trivial set
for B being set st not A /\ B is empty holds
A c= B

proof end;

theorem :: TEX_2:3

canceled;

theorem :: TEX_2:4

for S, T being 1-sorted st the carrier of S = the carrier of T & S is trivial holds
T is trivial

proof end;

definition

let S be set ;
let IT be Element of S;
attr IT is proper means :Def2: :: TEX_2:def 2
IT <> union S;

end;

:: deftheorem Def2 defines proper TEX_2:def 2 :

registration

let S be set ;
cluster non proper Element of K16(S);
existence

proof end;

end;

theorem Th5: :: TEX_2:5

for S being set
for A being Subset of S holds
( A is proper iff A <> S )

proof end;

registration

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

end;

registration

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

proof end;

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

proof end;

end;

registration

let S be non empty set ;
cluster proper Element of K16(S);
existence

proof end;

cluster non empty non proper Element of K16(S);
existence

proof end;

end;

registration

let S be non empty set ;
cluster non empty trivial Element of K16(S);
existence

proof end;

end;

registration

let y be set ;
cluster {y} -> trivial ;
coherence ;

end;

theorem :: TEX_2:6

for S being non empty set
for y being Element of S st {y} is proper holds
not S is trivial

proof end;

theorem :: TEX_2:7

for S being non empty non trivial set
for y being Element of S holds {y} is proper by Th5;

registration

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

end;

registration

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

end;

registration

let S be non empty non trivial set ;
cluster non empty trivial proper Element of K16(S);
existence

proof end;

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

proof end;

end;

theorem Th8: :: TEX_2:8

for Y being non empty 1-sorted
for y being Element of Y st {y} is proper holds
not Y is trivial

proof end;

theorem Th9: :: TEX_2:9

for Y being non empty non trivial 1-sorted
for y being Element of Y holds {y} is proper

proof end;

registration

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

proof end;

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

proof end;

end;

registration

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

proof end;

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

proof end;

end;

registration

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

proof end;

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

proof end;

end;

registration

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

proof end;

end;

theorem :: TEX_2:10

canceled;

theorem :: TEX_2:11

canceled;

theorem Th12: :: TEX_2:12

for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y1,the topology of Y1 #) & Y0 is TopSpace-like holds
Y1 is TopSpace-like

proof end;

definition

let Y be TopStruct ;
let IT be SubSpace of Y;
attr IT is proper means :Def3: :: TEX_2:def 3
for A being Subset of Y st A = the carrier of IT holds
A is proper;

end;

:: deftheorem Def3 defines proper TEX_2:def 3 :

theorem Th13: :: TEX_2:13

for Y being TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is proper iff Y0 is proper )

proof end;

Lm1: now

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

end;

theorem :: TEX_2:14

for Y being TopStruct
for Y0, Y1 being SubSpace of Y st TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y1,the topology of Y1 #) & Y0 is proper holds
Y1 is proper

proof end;

theorem Th15: :: TEX_2:15

for Y being TopStruct
for Y0 being SubSpace of Y st the carrier of Y0 = the carrier of Y holds
not Y0 is proper

proof end;

registration

let Y be non empty trivial TopStruct ;
cluster non empty -> non empty non proper SubSpace of Y;
coherence

proof end;

cluster non empty non proper -> non empty trivial SubSpace of Y;
coherence

proof end;

end;

registration

let Y be non empty non trivial TopStruct ;
cluster non empty trivial -> non empty proper SubSpace of Y;
coherence

proof end;

cluster non empty non proper -> non empty non trivial SubSpace of Y;
coherence

proof end;

end;

registration

let Y be non empty TopStruct ;
cluster non empty strict non proper SubSpace of Y;
existence

proof end;

end;

theorem :: TEX_2:16

for Y being non empty TopStruct
for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y,the topology of Y #)

proof end;

registration

let Y be non empty TopStruct ;
cluster discrete -> TopSpace-like SubSpace of Y;
coherence

proof end;

cluster anti-discrete -> TopSpace-like SubSpace of Y;
coherence

proof end;

cluster non TopSpace-like -> non discrete SubSpace of Y;
coherence

proof end;

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

proof end;

end;

theorem Th17: :: TEX_2:17

for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y1,the topology of Y1 #) & Y0 is discrete holds
Y1 is discrete

proof end;

theorem Th18: :: TEX_2:18

for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y1,the topology of Y1 #) & Y0 is anti-discrete holds
Y1 is anti-discrete

proof end;

registration

let Y be non empty TopStruct ;
cluster discrete -> almost_discrete SubSpace of Y;
coherence

proof end;

cluster non almost_discrete -> non discrete SubSpace of Y;
coherence

proof end;

cluster anti-discrete -> almost_discrete SubSpace of Y;
coherence

proof end;

cluster non almost_discrete -> non anti-discrete SubSpace of Y;
coherence

proof end;

end;

theorem :: TEX_2:19

for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y1,the topology of Y1 #) & Y0 is almost_discrete holds
Y1 is almost_discrete

proof end;

registration

let Y be non empty TopStruct ;
cluster non empty discrete anti-discrete -> non empty trivial SubSpace of Y;
coherence

proof end;

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

proof end;

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

proof end;

end;

definition

let Y be non empty TopStruct ;
let y be Point of Y;
func Sspace y -> non empty strict SubSpace of Y means :Def4: :: TEX_2:def 4
the carrier of it = {y};
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Sspace TEX_2:def 4 :

Lm2: now

let Y be non empty TopStruct ; :: thesis:
let y be Point of Y; :: thesis:
set Y0 = Sspace y;
the carrier of (Sspace y) = {y} by Def4;
then reconsider y0 = y as Point of (Sspace y) by TARSKI:def 1;
the carrier of (Sspace y) = {y0} by Def4;
hence Sspace y is trivial by TEX_1:def 1; :: thesis:

end;

registration

let Y be non empty TopStruct ;
cluster non empty strict trivial SubSpace of Y;
existence

proof end;

end;

registration

let Y be non empty TopStruct ;
let y be Point of Y;
cluster Sspace y -> non empty strict trivial ;
coherence by Lm2;

end;

theorem Th20: :: TEX_2:20

for Y being non empty TopStruct
for y being Point of Y holds
( Sspace y is proper iff {y} is proper )

proof end;

theorem :: TEX_2:21

for Y being non empty TopStruct
for y being Point of Y st Sspace y is proper holds
not Y is trivial

proof end;

registration

let Y be non empty non trivial TopStruct ;
cluster non empty strict trivial proper SubSpace of Y;
existence

proof end;

end;

theorem :: TEX_2:22

canceled;

theorem Th23: :: TEX_2:23

for Y being non empty TopStruct
for Y0 being non empty trivial SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of (Sspace y),the topology of (Sspace y) #)

proof end;

theorem Th24: :: TEX_2:24

for Y being non empty TopStruct
for y being Point of Y st Sspace y is TopSpace-like holds
( Sspace y is discrete & Sspace y is anti-discrete )

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let X be non empty TopSpace;
let x be Point of X;
cluster Sspace x -> non empty strict TopSpace-like discrete anti-discrete almost_discrete trivial ;
coherence ;

end;

registration

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

proof end;

end;

registration

let X be non empty TopSpace;
let x be Point of X;
cluster Sspace x -> non empty strict TopSpace-like discrete anti-discrete almost_discrete trivial ;
coherence ;

end;

registration

let X be non empty TopSpace;
cluster non proper -> open closed SubSpace of X;
coherence

proof end;

cluster non open -> proper SubSpace of X;
coherence

proof end;

cluster non closed -> proper SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty TopSpace;
cluster strict open closed SubSpace of X;
existence

proof end;

end;

registration

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

proof end;

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

cluster non empty non trivial -> non empty non discrete SubSpace of X;
coherence

proof end;

end;

registration

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

proof end;

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

end;

registration

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

proof end;

end;

registration

let X be non empty almost_discrete non trivial TopSpace;
cluster non empty strict almost_discrete proper SubSpace of X;
existence

proof end;

end;

definition

let Y be TopStruct ;
let IT be Subset of Y;
attr IT is discrete means :Def5: :: TEX_2:def 5
for D being Subset of Y st D c= IT holds
ex G being Subset of Y st
( G is open & IT /\ G = D );

end;

:: deftheorem Def5 defines discrete TEX_2:def 5 :

definition

let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is discrete means :Def6: :: TEX_2:def 6
for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D );
compatibility

proof end;

end;

:: deftheorem Def6 defines discrete TEX_2:def 6 :

theorem Th25: :: TEX_2:25

for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y1,the topology of Y1 #) & D0 = D1 & D0 is discrete holds
D1 is discrete

proof end;

theorem Th26: :: TEX_2:26

for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )

proof end;

theorem Th27: :: TEX_2:27

for Y being non empty TopStruct
for A being Subset of Y st A = the carrier of Y holds
( A is discrete iff Y is discrete )

proof end;

theorem Th28: :: TEX_2:28

for Y being TopStruct
for A, B being Subset of Y st B c= A & A is discrete holds
B is discrete

proof end;

theorem :: TEX_2:29

for Y being TopStruct
for A, B being Subset of Y st ( A is discrete or B is discrete ) holds
A /\ B is discrete

proof end;

theorem Th30: :: TEX_2:30

for Y being TopStruct st ( for P, Q being Subset of Y st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ) holds
for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete

proof end;

theorem Th31: :: TEX_2:31

for Y being TopStruct st ( for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ) holds
for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete

proof end;

theorem Th32: :: TEX_2:32

for Y being TopStruct
for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} )

proof end;

theorem :: TEX_2:33

for Y being TopStruct
for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )

proof end;

theorem Th34: :: TEX_2:34

for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is discrete holds
ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0

proof end;

theorem Th35: :: TEX_2:35

for X being non empty TopSpace
for A being empty Subset of X holds A is discrete

proof end;

theorem Th36: :: TEX_2:36

for X being non empty TopSpace
for x being Point of X holds {x} is discrete

proof end;

theorem Th37: :: TEX_2:37

for X being non empty TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) holds
A is discrete

proof end;

theorem :: TEX_2:38

for X being non empty TopSpace
for A, B being Subset of X st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete

proof end;

theorem :: TEX_2:39

for X being non empty TopSpace
for A, B being Subset of X st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete

proof end;

Lm3: for P, Q being set st P c= Q & P <> Q holds
Q \ P <> {}

proof end;

theorem :: TEX_2:40

for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense & A is discrete holds
A is open

proof end;

theorem Th41: :: TEX_2:41

for X being non empty TopSpace
for A being Subset of X holds
( A is discrete iff for D being Subset of X st D c= A holds
A /\ (Cl D) = D )

proof end;

theorem Th42: :: TEX_2:42

for X being non empty TopSpace
for A being Subset of X st A is discrete holds
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}

proof end;

theorem :: TEX_2:43

for X being non empty discrete TopSpace
for A being Subset of X holds A is discrete

proof end;

theorem Th44: :: TEX_2:44

for X being non empty anti-discrete TopSpace
for A being non empty Subset of X holds
( A is discrete iff A is trivial )

proof end;

definition

let Y be TopStruct ;
let IT be Subset of Y;
attr IT is maximal_discrete means :Def7: :: TEX_2:def 7
( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds
IT = D ) );

end;

:: deftheorem Def7 defines maximal_discrete TEX_2:def 7 :

theorem :: TEX_2:45

proof end;

theorem Th46: :: TEX_2:46

for X being non empty TopSpace
for A being empty Subset of X holds not A is maximal_discrete

proof end;

theorem Th47: :: TEX_2:47

for X being non empty TopSpace
for A being Subset of X st A is open & A is maximal_discrete holds
A is dense

proof end;

theorem :: TEX_2:48

for X being non empty TopSpace
for A being Subset of X st A is dense & A is discrete holds
A is maximal_discrete

proof end;

theorem Th49: :: TEX_2:49

for X being non empty discrete TopSpace
for A being Subset of X holds
( A is maximal_discrete iff not A is proper )

proof end;

theorem Th50: :: TEX_2:50

for X being non empty anti-discrete TopSpace
for A being non empty Subset of X holds
( A is maximal_discrete iff A is trivial )

proof end;

definition

let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attr IT is maximal_discrete means :Def8: :: TEX_2:def 8
for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete;

end;

:: deftheorem Def8 defines maximal_discrete TEX_2:def 8 :

theorem Th51: :: TEX_2:51

for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_discrete iff Y0 is maximal_discrete )

proof end;

registration

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

proof end;

cluster non empty non discrete -> non empty non maximal_discrete SubSpace of Y;
coherence

proof end;

end;

theorem :: TEX_2:52

for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0,the topology of X0 #) = TopStruct(# the carrier of Y0,the topology of Y0 #) ) ) )

proof end;

theorem Th53: :: TEX_2:53

for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is maximal_discrete holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_discrete & A0 = the carrier of X0 )

proof end;

registration

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

proof end;

cluster proper -> non maximal_discrete SubSpace of X;
coherence

proof end;

cluster non proper -> maximal_discrete SubSpace of X;
coherence

proof end;

cluster non maximal_discrete -> proper SubSpace of X;
coherence

proof end;

end;

registration

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

proof end;

cluster non empty non trivial -> non empty non maximal_discrete SubSpace of X;
coherence

proof end;

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

proof end;

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

proof end;

end;

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

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

provided

A1: for S being Subset of F₁() st S in F₂() holds
ex x being Point of F₁() st P₁[S,x]

proof end;

theorem Th54: :: TEX_2:54

for X being non empty almost_discrete TopSpace
for A being Subset of X holds Cl A = union { (Cl {a}) where a is Point of X : a in A }

proof end;

theorem Th55: :: TEX_2:55

for X being non empty almost_discrete TopSpace
for a, b being Point of X st a in Cl {b} holds
Cl {a} = Cl {b}

proof end;

theorem Th56: :: TEX_2:56

for X being non empty almost_discrete TopSpace
for a, b being Point of X holds
( Cl {a} misses Cl {b} or Cl {a} = Cl {b} )

proof end;

theorem Th57: :: TEX_2:57

for X being non empty almost_discrete TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ) holds
A is discrete

proof end;

theorem Th58: :: TEX_2:58

for X being non empty almost_discrete TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ) holds
A is discrete

proof end;

theorem :: TEX_2:59

for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} )

proof end;

theorem Th60: :: TEX_2:60

for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is discrete iff for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )

proof end;

theorem :: TEX_2:61

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

proof end;

theorem Th62: :: TEX_2:62

for X being non empty almost_discrete TopSpace
for A being Subset of X st A is maximal_discrete holds
A is dense

proof end;

theorem Th63: :: TEX_2:63

for X being non empty almost_discrete TopSpace
for A being Subset of X st A is maximal_discrete holds
union { (Cl {a}) where a is Point of X : a in A } = the carrier of X

proof end;

theorem Th64: :: TEX_2:64

for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is maximal_discrete iff for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )

proof end;

theorem Th65: :: TEX_2:65

for X being non empty almost_discrete TopSpace
for A being Subset of X st A is discrete holds
ex M being Subset of X st
( A c= M & M is maximal_discrete )

proof end;

theorem Th66: :: TEX_2:66

for X being non empty almost_discrete TopSpace ex M being Subset of X st M is maximal_discrete

proof end;

theorem Th67: :: TEX_2:67

for X being non empty almost_discrete TopSpace
for Y0 being non empty discrete SubSpace of X ex X0 being non empty strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_discrete )

proof end;

registration

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

proof end;

cluster non empty non proper -> non empty non maximal_discrete SubSpace of X;
coherence

proof end;

end;

registration

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

proof end;

cluster non empty trivial -> non empty non maximal_discrete SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty almost_discrete TopSpace;
cluster non empty strict discrete almost_discrete maximal_discrete SubSpace of X;
existence

proof end;

end;

theorem Th68: :: TEX_2:68

for X being discrete TopSpace
for Y being TopSpace
for f being Function of X,Y holds f is continuous

proof end;

theorem :: TEX_2:69

for X being non empty TopSpace st ( for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ) holds
X is discrete

proof end;

theorem :: TEX_2:70

for X being non empty TopSpace
for Y being non empty anti-discrete TopSpace
for f being Function of X,Y holds f is continuous

proof end;

theorem :: TEX_2:71

for Y being non empty TopSpace st ( for X being non empty TopSpace
for f being Function of X,Y holds f is continuous ) holds
Y is anti-discrete

proof end;

theorem Th72: :: TEX_2:72

for X being non empty discrete TopSpace
for X0 being non empty SubSpace of X ex r being continuous Function of X,X0 st r is_a_retraction

proof end;

theorem :: TEX_2:73

for X being non empty discrete TopSpace
for X0 being non empty SubSpace of X holds X0 is_a_retract_of X

proof end;

theorem Th74: :: TEX_2:74

for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X ex r being continuous Function of X,X0 st r is_a_retraction

proof end;

theorem :: TEX_2:75

for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X holds X0 is_a_retract_of X

proof end;

Lm4: for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}

proof end;

theorem Th76: :: TEX_2:76

for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E

proof end;

theorem :: TEX_2:77

for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
r " {a} = Cl {b} by Th76;

theorem Th78: :: TEX_2:78

for X being non empty almost_discrete TopSpace
for X0 being non empty discrete SubSpace of X ex r being continuous Function of X,X0 st r is_a_retraction

proof end;

theorem :: TEX_2:79

for X being non empty almost_discrete TopSpace
for X0 being non empty discrete SubSpace of X holds X0 is_a_retract_of X

proof end;