:: TEX_4 semantic presentation

registration

let X be non empty TopSpace;
let A be non empty Subset of X;
cluster Cl A -> non empty ;
coherence by PCOMPS_1:2;

end;

registration

let X be non empty TopSpace;
let A be empty Subset of X;
cluster Cl A -> empty ;
coherence by PRE_TOPC:52;

end;

registration

let X be non empty TopSpace;
let A be non proper Subset of X;
cluster Cl A -> non empty non proper ;
coherence

proof end;

end;

registration

let X be non empty non trivial TopSpace;
let A be non empty non trivial Subset of X;
cluster Cl A -> non empty non trivial ;
coherence

proof end;

end;

theorem Th1: :: TEX_4:1

for X being non empty TopSpace
for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }

proof end;

theorem Th2: :: TEX_4:2

for X being non empty TopSpace
for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }

proof end;

registration

let X be non empty TopSpace;
let A be non proper Subset of X;
cluster Int A -> non proper ;
coherence

proof end;

end;

registration

let X be non empty TopSpace;
let A be proper Subset of X;
cluster Int A -> proper ;
coherence

proof end;

end;

registration

let X be non empty TopSpace;
let A be empty Subset of X;
cluster Int A -> empty proper ;
coherence ;

end;

theorem :: TEX_4:3

canceled;

theorem :: TEX_4:4

for X being non empty TopSpace
for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) }

proof end;

definition

let Y be TopStruct ;
let IT be Subset of Y;
attr IT is anti-discrete means :Def1: :: TEX_4:def 1
for x being Point of Y
for G being Subset of Y st G is open & x in G & x in IT holds
IT c= G;

end;

:: deftheorem Def1 defines anti-discrete TEX_4:def 1 :

definition

let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete means :Def2: :: TEX_4:def 2
for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F;
compatibility

proof end;

end;

:: deftheorem Def2 defines anti-discrete TEX_4:def 2 :

definition

let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete means :Def3: :: TEX_4:def 3
for G being Subset of Y holds
( not G is open or A misses G or A c= G );
compatibility

proof end;

end;

:: deftheorem Def3 defines anti-discrete TEX_4:def 3 :

definition

let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete means :Def4: :: TEX_4:def 4
for F being Subset of Y holds
( not F is closed or A misses F or A c= F );
compatibility

proof end;

end;

:: deftheorem Def4 defines anti-discrete TEX_4:def 4 :

theorem :: TEX_4:5

canceled;

theorem Th6: :: TEX_4:6

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 anti-discrete holds
D1 is anti-discrete

proof end;

theorem Th7: :: TEX_4:7

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

proof end;

theorem Th8: :: TEX_4:8

for Y being non empty TopStruct
for x being Point of Y holds {x} is anti-discrete

proof end;

theorem Th9: :: TEX_4:9

for Y being non empty TopStruct
for A being empty Subset of Y holds A is anti-discrete

proof end;

definition

let Y be TopStruct ;
let IT be Subset-Family of Y;
attr IT is anti-discrete-set-family means :Def5: :: TEX_4:def 5
for A being Subset of Y st A in IT holds
A is anti-discrete;

end;

:: deftheorem Def5 defines anti-discrete-set-family TEX_4:def 5 :

theorem Th10: :: TEX_4:10

for Y being non empty TopStruct
for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds
union F is anti-discrete

proof end;

theorem :: TEX_4:11

for Y being non empty TopStruct
for F being Subset-Family of Y st F is anti-discrete-set-family holds
meet F is anti-discrete

proof end;

definition

let Y be TopStruct ;
let x be Point of Y;
func MaxADSF x -> Subset-Family of Y equals :: TEX_4:def 6
{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
coherence

proof end;

end;

:: deftheorem defines MaxADSF TEX_4:def 6 :

registration

let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSF x -> non empty ;
coherence

proof end;

end;

theorem Th12: :: TEX_4:12

for Y being non empty TopStruct
for x being Point of Y holds MaxADSF x is anti-discrete-set-family

proof end;

theorem Th13: :: TEX_4:13

for Y being non empty TopStruct
for x being Point of Y holds {x} = meet (MaxADSF x)

proof end;

theorem Th14: :: TEX_4:14

for Y being non empty TopStruct
for x being Point of Y holds {x} c= union (MaxADSF x)

proof end;

theorem Th15: :: TEX_4:15

for Y being non empty TopStruct
for x being Point of Y holds union (MaxADSF x) is anti-discrete

proof end;

definition

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

end;

:: deftheorem Def7 defines maximal_anti-discrete TEX_4:def 7 :

theorem :: TEX_4:16

proof end;

theorem Th17: :: TEX_4:17

for Y being non empty TopStruct
for A being empty Subset of Y holds not A is maximal_anti-discrete

proof end;

theorem Th18: :: TEX_4:18

for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & A is open holds
A is maximal_anti-discrete

proof end;

theorem Th19: :: TEX_4:19

for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & A is closed holds
A is maximal_anti-discrete

proof end;

definition

let Y be TopStruct ;
let x be Point of Y;
func MaxADSet x -> Subset of Y equals :: TEX_4:def 8
union (MaxADSF x);
coherence ;

end;

:: deftheorem defines MaxADSet TEX_4:def 8 :

registration

let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSet x -> non empty ;
coherence

proof end;

end;

theorem Th20: :: TEX_4:20

for Y being non empty TopStruct
for x being Point of Y holds {x} c= MaxADSet x by Th14;

theorem Th21: :: TEX_4:21

for Y being non empty TopStruct
for D being Subset of Y
for x being Point of Y st D is anti-discrete & x in D holds
D c= MaxADSet x

proof end;

theorem Th22: :: TEX_4:22

for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x is maximal_anti-discrete

proof end;

theorem Th23: :: TEX_4:23

for Y being non empty TopStruct
for x, y being Point of Y holds
( y in MaxADSet x iff MaxADSet y = MaxADSet x )

proof end;

theorem Th24: :: TEX_4:24

for Y being non empty TopStruct
for x, y being Point of Y holds
( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )

proof end;

theorem Th25: :: TEX_4:25

for Y being non empty TopStruct
for F being Subset of Y
for x being Point of Y st F is closed & x in F holds
MaxADSet x c= F

proof end;

theorem Th26: :: TEX_4:26

for Y being non empty TopStruct
for G being Subset of Y
for x being Point of Y st G is open & x in G holds
MaxADSet x c= G

proof end;

theorem :: TEX_4:27

for Y being non empty TopStruct
for x being Point of Y st { F where F is Subset of Y : ( F is closed & x in F ) } <> {} holds
MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) }

proof end;

theorem :: TEX_4:28

for Y being non empty TopStruct
for x being Point of Y st { G where G is Subset of Y : ( G is open & x in G ) } <> {} holds
MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }

proof end;

definition

let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is maximal_anti-discrete means :Def9: :: TEX_4:def 9
ex x being Point of Y st
( x in A & A = MaxADSet x );
compatibility

proof end;

end;

:: deftheorem Def9 defines maximal_anti-discrete TEX_4:def 9 :

theorem Th29: :: TEX_4:29

for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st x in A & A is maximal_anti-discrete holds
A = MaxADSet x

proof end;

definition

let Y be non empty TopStruct ;
let A be non empty Subset of Y;
redefine attr A is maximal_anti-discrete means :: TEX_4:def 10
for x being Point of Y st x in A holds
A = MaxADSet x;
compatibility

proof end;

end;

:: deftheorem defines maximal_anti-discrete TEX_4:def 10 :

definition

let Y be non empty TopStruct ;
let A be Subset of Y;
func MaxADSet A -> Subset of Y equals :: TEX_4:def 11
union { (MaxADSet a) where a is Point of Y : a in A } ;
coherence

proof end;

end;

:: deftheorem defines MaxADSet TEX_4:def 11 :

theorem Th30: :: TEX_4:30

for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x = MaxADSet {x}

proof end;

theorem Th31: :: TEX_4:31

for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x meets A

proof end;

theorem Th32: :: TEX_4:32

for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A

proof end;

theorem Th33: :: TEX_4:33

for Y being non empty TopStruct
for A, B being Subset of Y st A c= B holds
MaxADSet A c= MaxADSet B

proof end;

theorem Th34: :: TEX_4:34

for Y being non empty TopStruct
for A being Subset of Y holds A c= MaxADSet A

proof end;

theorem Th35: :: TEX_4:35

for Y being non empty TopStruct
for A being Subset of Y holds MaxADSet A = MaxADSet (MaxADSet A)

proof end;

theorem Th36: :: TEX_4:36

for Y being non empty TopStruct
for A, B being Subset of Y st A c= MaxADSet B holds
MaxADSet A c= MaxADSet B

proof end;

theorem Th37: :: TEX_4:37

for Y being non empty TopStruct
for A, B being Subset of Y holds
( ( B c= MaxADSet A & A c= MaxADSet B ) iff MaxADSet A = MaxADSet B )

proof end;

theorem :: TEX_4:38

for Y being non empty TopStruct
for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)

proof end;

theorem Th39: :: TEX_4:39

for Y being non empty TopStruct
for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)

proof end;

registration

let Y be non empty TopStruct ;
let A be non empty Subset of Y;
cluster MaxADSet A -> non empty ;
coherence

proof end;

end;

registration

let Y be non empty TopStruct ;
let A be empty Subset of Y;
cluster MaxADSet A -> empty ;
coherence

proof end;

end;

registration

let Y be non empty TopStruct ;
let A be non proper Subset of Y;
cluster MaxADSet A -> non empty non proper ;
coherence

proof end;

end;

registration

let Y be non empty non trivial TopStruct ;
let A be non empty non trivial Subset of Y;
cluster MaxADSet A -> non empty non trivial ;
coherence

proof end;

end;

theorem Th40: :: TEX_4:40

for Y being non empty TopStruct
for G, A being Subset of Y st G is open & A c= G holds
MaxADSet A c= G

proof end;

theorem Th41: :: TEX_4:41

for Y being non empty TopStruct
for A being Subset of Y st { G where G is Subset of Y : ( G is open & A c= G ) } <> {} holds
MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }

proof end;

theorem Th42: :: TEX_4:42

for Y being non empty TopStruct
for F, A being Subset of Y st F is closed & A c= F holds
MaxADSet A c= F

proof end;

theorem Th43: :: TEX_4:43

for Y being non empty TopStruct
for A being Subset of Y st { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} holds
MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) }

proof end;

definition

let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :Def12: :: TEX_4:def 12
for x being Point of X st x in A holds
A c= Cl {x};
compatibility

proof end;

end;

:: deftheorem Def12 defines anti-discrete TEX_4:def 12 :

definition

let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :: TEX_4:def 13
for x being Point of X st x in A holds
Cl A = Cl {x};
compatibility

proof end;

end;

:: deftheorem defines anti-discrete TEX_4:def 13 :

definition

let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :Def14: :: TEX_4:def 14
for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y};
compatibility

proof end;

end;

:: deftheorem Def14 defines anti-discrete TEX_4:def 14 :

theorem :: TEX_4:44

for X being non empty TopSpace
for x being Point of X
for D being Subset of X st D is anti-discrete & Cl {x} c= D holds
D = Cl {x}

proof end;

theorem :: TEX_4:45

for X being non empty TopSpace
for A being Subset of X holds
( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds
A = Cl {x} )

proof end;

theorem :: TEX_4:46

for X being non empty TopSpace
for A being Subset of X st A is anti-discrete & not A is open holds
A is boundary

proof end;

theorem Th47: :: TEX_4:47

for X being non empty TopSpace
for x being Point of X st Cl {x} = {x} holds
{x} is maximal_anti-discrete

proof end;

theorem Th48: :: TEX_4:48

for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }

proof end;

theorem Th49: :: TEX_4:49

for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }

proof end;

theorem Th50: :: TEX_4:50

for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= Cl {x}

proof end;

Lm1: for X being non empty TopSpace
for x, y being Point of X st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}

proof end;

theorem Th51: :: TEX_4:51

for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )

proof end;

theorem :: TEX_4:52

for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} )

proof end;

definition

let X be non empty TopSpace;
let x be Point of X;
:: original: MaxADSet
redefine func MaxADSet x -> non empty Subset of X equals :: TEX_4:def 15
(Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } );
compatibility

proof end;

coherence ;

end;

:: deftheorem defines MaxADSet TEX_4:def 15 :

theorem Th53: :: TEX_4:53

for X being non empty TopSpace
for x, y being Point of X holds
( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } )

proof end;

theorem :: TEX_4:54

for X being non empty TopSpace
for x, y being Point of X holds
( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )

proof end;

theorem Th55: :: TEX_4:55

for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )

proof end;

theorem :: TEX_4:56

for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )

proof end;

theorem Th57: :: TEX_4:57

for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) }

proof end;

theorem Th58: :: TEX_4:58

for X being non empty TopSpace
for P being Subset of X st P is open holds
MaxADSet P = P

proof end;

theorem :: TEX_4:59

for X being non empty TopSpace
for A being Subset of X holds MaxADSet (Int A) = Int A by Th58;

theorem Th60: :: TEX_4:60

for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) }

proof end;

theorem Th61: :: TEX_4:61

for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= Cl A

proof end;

theorem Th62: :: TEX_4:62

for X being non empty TopSpace
for P being Subset of X st P is closed holds
MaxADSet P = P

proof end;

theorem :: TEX_4:63

for X being non empty TopSpace
for A being Subset of X holds MaxADSet (Cl A) = Cl A by Th62;

theorem :: TEX_4:64

for X being non empty TopSpace
for A being Subset of X holds Cl (MaxADSet A) = Cl A

proof end;

theorem :: TEX_4:65

for X being non empty TopSpace
for A, B being Subset of X st MaxADSet A = MaxADSet B holds
Cl A = Cl B

proof end;

theorem :: TEX_4:66

for X being non empty TopSpace
for P, Q being Subset of X st ( P is closed or Q is closed ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

proof end;

theorem :: TEX_4:67

for X being non empty TopSpace
for P, Q being Subset of X st ( P is open or Q is open ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

proof end;

theorem Th68: :: TEX_4:68

for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds
A is anti-discrete

proof end;

theorem Th69: :: TEX_4:69

for Y being non empty TopStruct
for Y0 being SubSpace of Y st Y0 is TopSpace-like holds
for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete

proof end;

theorem :: TEX_4:70

for X being non empty TopSpace
for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete

proof end;

theorem :: TEX_4:71

for X being non empty TopSpace
for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete

proof end;

theorem :: TEX_4:72

for X being non empty TopSpace
for Y0 being anti-discrete SubSpace of X
for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )

proof end;

theorem :: TEX_4:73

for X being non empty TopSpace
for Y0 being anti-discrete SubSpace of X
for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )

proof end;

definition

let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attr IT is maximal_anti-discrete means :Def16: :: TEX_4:def 16
( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds
the carrier of IT = the carrier of Y0 ) );

end;

:: deftheorem Def16 defines maximal_anti-discrete TEX_4:def 16 :

registration

let Y be non empty TopStruct ;
cluster maximal_anti-discrete -> anti-discrete SubSpace of Y;
coherence by Def16;
cluster non anti-discrete -> non maximal_anti-discrete SubSpace of Y;
coherence by Def16;

end;

theorem Th74: :: TEX_4:74

for X being non empty TopSpace
for Y0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of Y0 holds
( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

proof end;

registration

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

definition

let Y be TopStruct ;
let x be Point of Y;
func MaxADSspace x -> strict SubSpace of Y means :Def17: :: TEX_4:def 17
the carrier of it = MaxADSet x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines MaxADSspace TEX_4:def 17 :

registration

let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSspace x -> non empty strict ;
coherence

proof end;

end;

Lm2: for Y being non empty TopStruct
for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds
X1 is SubSpace of X2

proof end;

theorem :: TEX_4:75

for Y being non empty TopStruct
for x being Point of Y holds Sspace x is SubSpace of MaxADSspace x

proof end;

theorem :: TEX_4:76

for Y being non empty TopStruct
for x, y being Point of Y holds
( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y),the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) )

proof end;

theorem :: TEX_4:77

for Y being non empty TopStruct
for x, y being Point of Y holds
( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y),the topology of (MaxADSspace y) #) )

proof end;

registration

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

proof end;

end;

registration

let X be non empty TopSpace;
let x be Point of X;
cluster MaxADSspace x -> non empty strict anti-discrete maximal_anti-discrete ;
coherence

proof end;

end;

theorem :: TEX_4:78

for X being non empty TopSpace
for X0 being non empty closed SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0

proof end;

theorem :: TEX_4:79

for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0

proof end;

theorem :: TEX_4:80

for X being non empty TopSpace
for x being Point of X st Cl {x} = {x} holds
Sspace x is maximal_anti-discrete

proof end;

definition

let Y be TopStruct ;
let A be Subset of Y;
func Sspace A -> strict SubSpace of Y means :Def18: :: TEX_4:def 18
the carrier of it = A;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Sspace TEX_4:def 18 :

registration

let Y be non empty TopStruct ;
let A be non empty Subset of Y;
cluster Sspace A -> non empty strict ;
coherence

proof end;

end;

theorem :: TEX_4:81

for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (Sspace A)

proof end;

theorem :: TEX_4:82

for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0

proof end;

registration

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

proof end;

end;

registration

let Y be non empty non trivial TopStruct ;
let A be non empty non trivial Subset of Y;
cluster Sspace A -> non empty non trivial strict ;
coherence

proof end;

end;

registration

let Y be non empty TopStruct ;
let A be non empty non proper Subset of Y;
cluster Sspace A -> non empty strict non proper ;
coherence

proof end;

end;

definition

let Y be non empty TopStruct ;
let A be Subset of Y;
func MaxADSspace A -> strict SubSpace of Y means :Def19: :: TEX_4:def 19
the carrier of it = MaxADSet A;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines MaxADSspace TEX_4:def 19 :

registration

let Y be non empty TopStruct ;
let A be non empty Subset of Y;
cluster MaxADSspace A -> non empty strict ;
coherence

proof end;

end;

theorem :: TEX_4:83

for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (MaxADSspace A)

proof end;

theorem :: TEX_4:84

for Y being non empty TopStruct
for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A

proof end;

theorem :: TEX_4:85

for Y being non empty TopStruct
for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x),the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}),the topology of (MaxADSspace {x}) #)

proof end;

theorem :: TEX_4:86

for Y being non empty TopStruct
for A, B being non empty Subset of Y st A c= B holds
MaxADSspace A is SubSpace of MaxADSspace B

proof end;

theorem :: TEX_4:87

for Y being non empty TopStruct
for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A),the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)),the topology of (MaxADSspace (MaxADSet A)) #)

proof end;

theorem :: TEX_4:88

for Y being non empty TopStruct
for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds
MaxADSspace A is SubSpace of MaxADSspace B

proof end;

theorem :: TEX_4:89

for Y being non empty TopStruct
for A, B being non empty Subset of Y holds
( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A),the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B),the topology of (MaxADSspace B) #) )

proof end;

registration

let Y be non empty non trivial TopStruct ;
let A be non empty non trivial Subset of Y;
cluster MaxADSspace A -> non empty non trivial strict ;
coherence

proof end;

end;

registration

let Y be non empty TopStruct ;
let A be non empty non proper Subset of Y;
cluster MaxADSspace A -> non empty strict non proper ;
coherence

proof end;

end;

theorem :: TEX_4:90

for X being non empty TopSpace
for X0 being open SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0

proof end;

theorem :: TEX_4:91

for X being non empty TopSpace
for X0 being closed SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0

proof end;