:: TEX_4 semantic presentation

registration

let c₁ be non empty TopSpace;
let c₂ be non empty Subset of c₁;
cluster Cl a₂ -> non empty ;
coherence by PCOMPS_1:2;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be empty Subset of c₁;
cluster Cl a₂ -> empty ;
coherence by PRE_TOPC:52;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non proper Subset of c₁;
cluster Cl a₂ -> non empty non proper ;
coherence

proof end;

end;

registration

let c₁ be non empty non trivial TopSpace;
let c₂ be non empty non trivial Subset of c₁;
cluster Cl a₂ -> non empty non trivial ;
coherence

proof end;

end;

theorem Th1: :: TEX_4:1

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds Cl b₂ = meet { b₃ where B is Subset of b₁ : ( b₃ is closed & b₂ c= b₃ ) }

proof end;

theorem Th2: :: TEX_4:2

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

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be non proper Subset of c₁;
cluster Int a₂ -> non proper ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be proper Subset of c₁;
cluster Int a₂ -> proper ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be empty Subset of c₁;
cluster Int a₂ -> empty proper ;
coherence ;

end;

theorem Th3: :: TEX_4:3

canceled;

theorem Th4: :: TEX_4:4

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds Int b₂ = union { b₃ where B is Subset of b₁ : ( b₃ is open & b₃ c= b₂ ) }

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is anti-discrete means :Def1: :: TEX_4:def 1
for b₁ being Point of a₁
for b₂ being Subset of a₁ st b₂ is open & b₁ in b₂ & b₁ in a₂ holds
a₂ c= b₂;

end;

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

definition

let c₁ be non empty TopStruct ;
let c₂ be Subset of c₁;
redefine attr a₂ is anti-discrete means :Def2: :: TEX_4:def 2
for b₁ being Point of a₁
for b₂ being Subset of a₁ st b₂ is closed & b₁ in b₂ & b₁ in a₂ holds
a₂ c= b₂;
compatibility

proof end;

end;

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

definition

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

proof end;

end;

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

definition

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

proof end;

end;

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

theorem Th5: :: TEX_4:5

canceled;

theorem Th6: :: TEX_4:6

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

proof end;

theorem Th7: :: TEX_4:7

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

proof end;

theorem Th8: :: TEX_4:8

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds {b₂} is anti-discrete

proof end;

theorem Th9: :: TEX_4:9

for b₁ being non empty TopStruct
for b₂ being empty Subset of b₁ holds b₂ is anti-discrete

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset-Family of c₁;
attr a₂ is anti-discrete-set-family means :Def5: :: TEX_4:def 5
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ is anti-discrete;

end;

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

theorem Th10: :: TEX_4:10

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

proof end;

theorem Th11: :: TEX_4:11

for b₁ being non empty TopStruct
for b₂ being Subset-Family of b₁ st b₂ is anti-discrete-set-family holds
meet b₂ is anti-discrete

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Point of c₁;
func MaxADSF c₂ -> Subset-Family of a₁ equals :: TEX_4:def 6
{ b₁ where B is Subset of a₁ : ( b₁ is anti-discrete & a₂ in b₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def6 defines MaxADSF TEX_4:def 6 :

registration

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
cluster MaxADSF a₂ -> non empty ;
coherence

proof end;

end;

theorem Th12: :: TEX_4:12

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds MaxADSF b₂ is anti-discrete-set-family

proof end;

theorem Th13: :: TEX_4:13

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds {b₂} = meet (MaxADSF b₂)

proof end;

theorem Th14: :: TEX_4:14

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds {b₂} c= union (MaxADSF b₂)

proof end;

theorem Th15: :: TEX_4:15

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds union (MaxADSF b₂) is anti-discrete

proof end;

definition

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

end;

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

theorem Th16: :: TEX_4:16

proof end;

theorem Th17: :: TEX_4:17

for b₁ being non empty TopStruct
for b₂ being empty Subset of b₁ holds not b₂ is maximal_anti-discrete

proof end;

theorem Th18: :: TEX_4:18

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ st b₂ is anti-discrete & b₂ is open holds
b₂ is maximal_anti-discrete

proof end;

theorem Th19: :: TEX_4:19

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ st b₂ is anti-discrete & b₂ is closed holds
b₂ is maximal_anti-discrete

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Point of c₁;
func MaxADSet c₂ -> Subset of a₁ equals :: TEX_4:def 8
union (MaxADSF a₂);
coherence ;

end;

:: deftheorem Def8 defines MaxADSet TEX_4:def 8 :

registration

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
cluster MaxADSet a₂ -> non empty ;
coherence

proof end;

end;

theorem Th20: :: TEX_4:20

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds {b₂} c= MaxADSet b₂ by Th14;

theorem Th21: :: TEX_4:21

for b₁ being non empty TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is anti-discrete & b₃ in b₂ holds
b₂ c= MaxADSet b₃

proof end;

theorem Th22: :: TEX_4:22

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds MaxADSet b₂ is maximal_anti-discrete

proof end;

theorem Th23: :: TEX_4:23

for b₁ being non empty TopStruct
for b₂, b₃ being Point of b₁ holds
( b₃ in MaxADSet b₂ iff MaxADSet b₃ = MaxADSet b₂ )

proof end;

theorem Th24: :: TEX_4:24

for b₁ being non empty TopStruct
for b₂, b₃ being Point of b₁ holds
( MaxADSet b₂ misses MaxADSet b₃ or MaxADSet b₂ = MaxADSet b₃ )

proof end;

theorem Th25: :: TEX_4:25

for b₁ being non empty TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is closed & b₃ in b₂ holds
MaxADSet b₃ c= b₂

proof end;

theorem Th26: :: TEX_4:26

for b₁ being non empty TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is open & b₃ in b₂ holds
MaxADSet b₃ c= b₂

proof end;

theorem Th27: :: TEX_4:27

for b₁ being non empty TopStruct
for b₂ being Point of b₁ st { b₃ where B is Subset of b₁ : ( b₃ is closed & b₂ in b₃ ) } <> {} holds
MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is closed & b₂ in b₃ ) }

proof end;

theorem Th28: :: TEX_4:28

for b₁ being non empty TopStruct
for b₂ being Point of b₁ st { b₃ where B is Subset of b₁ : ( b₃ is open & b₂ in b₃ ) } <> {} holds
MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is open & b₂ in b₃ ) }

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Subset of c₁;
redefine attr a₂ is maximal_anti-discrete means :Def9: :: TEX_4:def 9
ex b₁ being Point of a₁ st
( b₁ in a₂ & a₂ = MaxADSet b₁ );
compatibility

proof end;

end;

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

theorem Th29: :: TEX_4:29

for b₁ being non empty TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₃ in b₂ & b₂ is maximal_anti-discrete holds
b₂ = MaxADSet b₃

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be non empty Subset of c₁;
redefine attr a₂ is maximal_anti-discrete means :: TEX_4:def 10
for b₁ being Point of a₁ st b₁ in a₂ holds
a₂ = MaxADSet b₁;
compatibility

proof end;

end;

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

definition

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

proof end;

end;

:: deftheorem Def11 defines MaxADSet TEX_4:def 11 :

theorem Th30: :: TEX_4:30

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds MaxADSet b₂ = MaxADSet {b₂}

proof end;

theorem Th31: :: TEX_4:31

for b₁ being non empty TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ st MaxADSet b₃ meets MaxADSet b₂ holds
MaxADSet b₃ meets b₂

proof end;

theorem Th32: :: TEX_4:32

for b₁ being non empty TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ st MaxADSet b₃ meets MaxADSet b₂ holds
MaxADSet b₃ c= MaxADSet b₂

proof end;

theorem Th33: :: TEX_4:33

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
MaxADSet b₂ c= MaxADSet b₃

proof end;

theorem Th34: :: TEX_4:34

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ holds b₂ c= MaxADSet b₂

proof end;

theorem Th35: :: TEX_4:35

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ holds MaxADSet b₂ = MaxADSet (MaxADSet b₂)

proof end;

theorem Th36: :: TEX_4:36

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st b₂ c= MaxADSet b₃ holds
MaxADSet b₂ c= MaxADSet b₃

proof end;

theorem Th37: :: TEX_4:37

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ holds
( ( b₃ c= MaxADSet b₂ & b₂ c= MaxADSet b₃ ) iff MaxADSet b₂ = MaxADSet b₃ )

proof end;

theorem Th38: :: TEX_4:38

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ holds MaxADSet (b₂ \/ b₃) = (MaxADSet b₂) \/ (MaxADSet b₃)

proof end;

theorem Th39: :: TEX_4:39

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ holds MaxADSet (b₂ /\ b₃) c= (MaxADSet b₂) /\ (MaxADSet b₃)

proof end;

registration

let c₁ be non empty TopStruct ;
let c₂ be non empty Subset of c₁;
cluster MaxADSet a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
let c₂ be empty Subset of c₁;
cluster MaxADSet a₂ -> empty ;
coherence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
let c₂ be non proper Subset of c₁;
cluster MaxADSet a₂ -> non empty non proper ;
coherence

proof end;

end;

registration

let c₁ be non empty non trivial TopStruct ;
let c₂ be non empty non trivial Subset of c₁;
cluster MaxADSet a₂ -> non empty non trivial ;
coherence

proof end;

end;

theorem Th40: :: TEX_4:40

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ c= b₂ holds
MaxADSet b₃ c= b₂

proof end;

theorem Th41: :: TEX_4:41

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ st { b₃ where B is Subset of b₁ : ( b₃ is open & b₂ c= b₃ ) } <> {} holds
MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is open & b₂ c= b₃ ) }

proof end;

theorem Th42: :: TEX_4:42

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ c= b₂ holds
MaxADSet b₃ c= b₂

proof end;

theorem Th43: :: TEX_4:43

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ st { b₃ where B is Subset of b₁ : ( b₃ is closed & b₂ c= b₃ ) } <> {} holds
MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is closed & b₂ c= b₃ ) }

proof end;

definition

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

proof end;

end;

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

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is anti-discrete means :: TEX_4:def 13
for b₁ being Point of a₁ st b₁ in a₂ holds
Cl a₂ = Cl {b₁};
compatibility

proof end;

end;

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

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is anti-discrete means :Def14: :: TEX_4:def 14
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ holds
Cl {b₁} = Cl {b₂};
compatibility

proof end;

end;

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

theorem Th44: :: TEX_4:44

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁ st b₃ is anti-discrete & Cl {b₂} c= b₃ holds
b₃ = Cl {b₂}

proof end;

theorem Th45: :: TEX_4:45

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( ( b₂ is anti-discrete & b₂ is closed ) iff for b₃ being Point of b₁ st b₃ in b₂ holds
b₂ = Cl {b₃} )

proof end;

theorem Th46: :: TEX_4:46

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is anti-discrete & not b₂ is open holds
b₂ is boundary

proof end;

theorem Th47: :: TEX_4:47

for b₁ being non empty TopSpace
for b₂ being Point of b₁ st Cl {b₂} = {b₂} holds
{b₂} is maximal_anti-discrete

proof end;

theorem Th48: :: TEX_4:48

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is open & b₂ in b₃ ) }

proof end;

theorem Th49: :: TEX_4:49

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is closed & b₂ in b₃ ) }

proof end;

theorem Th50: :: TEX_4:50

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds MaxADSet b₂ c= Cl {b₂}

proof end;

Lemma49: for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ st MaxADSet b₂ = MaxADSet b₃ holds
Cl {b₂} = Cl {b₃}

proof end;

theorem Th51: :: TEX_4:51

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ holds
( MaxADSet b₂ = MaxADSet b₃ iff Cl {b₂} = Cl {b₃} )

proof end;

theorem Th52: :: TEX_4:52

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ holds
( MaxADSet b₂ misses MaxADSet b₃ iff Cl {b₂} <> Cl {b₃} )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
redefine func MaxADSet as MaxADSet c₂ -> non empty Subset of a₁ equals :: TEX_4:def 15
(Cl {a₂}) /\ (meet { b₁ where B is Subset of a₁ : ( b₁ is open & a₂ in b₁ ) } );
compatibility

proof end;

coherence ;

end;

:: deftheorem Def15 defines MaxADSet TEX_4:def 15 :

theorem Th53: :: TEX_4:53

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ holds
( Cl {b₂} c= Cl {b₃} iff meet { b₄ where B is Subset of b₁ : ( b₄ is open & b₃ in b₄ ) } c= meet { b₄ where B is Subset of b₁ : ( b₄ is open & b₂ in b₄ ) } )

proof end;

theorem Th54: :: TEX_4:54

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ holds
( Cl {b₂} c= Cl {b₃} iff MaxADSet b₃ c= meet { b₄ where B is Subset of b₁ : ( b₄ is open & b₂ in b₄ ) } )

proof end;

theorem Th55: :: TEX_4:55

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ holds
( MaxADSet b₂ misses MaxADSet b₃ iff ( ex b₄ being Subset of b₁ st
( b₄ is open & MaxADSet b₂ c= b₄ & b₄ misses MaxADSet b₃ ) or ex b₄ being Subset of b₁ st
( b₄ is open & b₄ misses MaxADSet b₂ & MaxADSet b₃ c= b₄ ) ) )

proof end;

theorem Th56: :: TEX_4:56

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ holds
( MaxADSet b₂ misses MaxADSet b₃ iff ( ex b₄ being Subset of b₁ st
( b₄ is closed & MaxADSet b₂ c= b₄ & b₄ misses MaxADSet b₃ ) or ex b₄ being Subset of b₁ st
( b₄ is closed & b₄ misses MaxADSet b₂ & MaxADSet b₃ c= b₄ ) ) )

proof end;

theorem Th57: :: TEX_4:57

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is open & b₂ c= b₃ ) }

proof end;

theorem Th58: :: TEX_4:58

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is open holds
MaxADSet b₂ = b₂

proof end;

theorem Th59: :: TEX_4:59

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds MaxADSet (Int b₂) = Int b₂ by Th58;

theorem Th60: :: TEX_4:60

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds MaxADSet b₂ c= meet { b₃ where B is Subset of b₁ : ( b₃ is closed & b₂ c= b₃ ) }

proof end;

theorem Th61: :: TEX_4:61

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds MaxADSet b₂ c= Cl b₂

proof end;

theorem Th62: :: TEX_4:62

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is closed holds
MaxADSet b₂ = b₂

proof end;

theorem Th63: :: TEX_4:63

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds MaxADSet (Cl b₂) = Cl b₂ by Th62;

theorem Th64: :: TEX_4:64

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds Cl (MaxADSet b₂) = Cl b₂

proof end;

theorem Th65: :: TEX_4:65

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st MaxADSet b₂ = MaxADSet b₃ holds
Cl b₂ = Cl b₃

proof end;

theorem Th66: :: TEX_4:66

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st ( b₂ is closed or b₃ is closed ) holds
MaxADSet (b₂ /\ b₃) = (MaxADSet b₂) /\ (MaxADSet b₃)

proof end;

theorem Th67: :: TEX_4:67

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st ( b₂ is open or b₃ is open ) holds
MaxADSet (b₂ /\ b₃) = (MaxADSet b₂) /\ (MaxADSet b₃)

proof end;

theorem Th68: :: TEX_4:68

for b₁ being non empty TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ & b₂ is anti-discrete holds
b₃ is anti-discrete

proof end;

theorem Th69: :: TEX_4:69

for b₁ being non empty TopStruct
for b₂ being SubSpace of b₁ st b₂ is TopSpace-like holds
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ & b₃ is anti-discrete holds
b₂ is anti-discrete

proof end;

theorem Th70: :: TEX_4:70

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ st ( for b₃ being open SubSpace of b₁ holds
( b₂ misses b₃ or b₂ is SubSpace of b₃ ) ) holds
b₂ is anti-discrete

proof end;

theorem Th71: :: TEX_4:71

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ st ( for b₃ being closed SubSpace of b₁ holds
( b₂ misses b₃ or b₂ is SubSpace of b₃ ) ) holds
b₂ is anti-discrete

proof end;

theorem Th72: :: TEX_4:72

for b₁ being non empty TopSpace
for b₂ being anti-discrete SubSpace of b₁
for b₃ being open SubSpace of b₁ holds
( b₂ misses b₃ or b₂ is SubSpace of b₃ )

proof end;

theorem Th73: :: TEX_4:73

for b₁ being non empty TopSpace
for b₂ being anti-discrete SubSpace of b₁
for b₃ being closed SubSpace of b₁ holds
( b₂ misses b₃ or b₂ is SubSpace of b₃ )

proof end;

definition

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

end;

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

registration

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

end;

theorem Th74: :: TEX_4:74

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

proof end;

registration

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

definition

let c₁ be TopStruct ;
let c₂ be Point of c₁;
func MaxADSspace c₂ -> strict SubSpace of a₁ means :Def17: :: TEX_4:def 17
the carrier of a₃ = MaxADSet a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines MaxADSspace TEX_4:def 17 :

registration

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
cluster MaxADSspace a₂ -> non empty strict ;
coherence

proof end;

end;

Lemma63: for b₁ being non empty TopStruct
for b₂, b₃ being SubSpace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is SubSpace of b₃

proof end;

theorem Th75: :: TEX_4:75

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds Sspace b₂ is SubSpace of MaxADSspace b₂

proof end;

theorem Th76: :: TEX_4:76

for b₁ being non empty TopStruct
for b₂, b₃ being Point of b₁ holds
( b₃ is Point of (MaxADSspace b₂) iff TopStruct(# the carrier of (MaxADSspace b₃),the topology of (MaxADSspace b₃) #) = TopStruct(# the carrier of (MaxADSspace b₂),the topology of (MaxADSspace b₂) #) )

proof end;

theorem Th77: :: TEX_4:77

for b₁ being non empty TopStruct
for b₂, b₃ being Point of b₁ holds
( the carrier of (MaxADSspace b₂) misses the carrier of (MaxADSspace b₃) or TopStruct(# the carrier of (MaxADSspace b₂),the topology of (MaxADSspace b₂) #) = TopStruct(# the carrier of (MaxADSspace b₃),the topology of (MaxADSspace b₃) #) )

proof end;

registration

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

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster MaxADSspace a₂ -> non empty strict anti-discrete maximal_anti-discrete ;
coherence

proof end;

end;

theorem Th78: :: TEX_4:78

for b₁ being non empty TopSpace
for b₂ being non empty closed SubSpace of b₁
for b₃ being Point of b₁ st b₃ is Point of b₂ holds
MaxADSspace b₃ is SubSpace of b₂

proof end;

theorem Th79: :: TEX_4:79

for b₁ being non empty TopSpace
for b₂ being non empty open SubSpace of b₁
for b₃ being Point of b₁ st b₃ is Point of b₂ holds
MaxADSspace b₃ is SubSpace of b₂

proof end;

theorem Th80: :: TEX_4:80

for b₁ being non empty TopSpace
for b₂ being Point of b₁ st Cl {b₂} = {b₂} holds
Sspace b₂ is maximal_anti-discrete

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
func Sspace c₂ -> strict SubSpace of a₁ means :Def18: :: TEX_4:def 18
the carrier of a₃ = a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Sspace TEX_4:def 18 :

registration

let c₁ be non empty TopStruct ;
let c₂ be non empty Subset of c₁;
cluster Sspace a₂ -> non empty strict ;
coherence

proof end;

end;

theorem Th81: :: TEX_4:81

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ holds b₂ is Subset of (Sspace b₂)

proof end;

theorem Th82: :: TEX_4:82

for b₁ being non empty TopStruct
for b₂ being SubSpace of b₁
for b₃ being non empty Subset of b₁ st b₃ is Subset of b₂ holds
Sspace b₃ is SubSpace of b₂

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be non empty TopStruct ;
let c₂ be non empty non proper Subset of c₁;
cluster Sspace a₂ -> non empty strict non proper ;
coherence

proof end;

end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Subset of c₁;
func MaxADSspace c₂ -> strict SubSpace of a₁ means :Def19: :: TEX_4:def 19
the carrier of a₃ = MaxADSet a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines MaxADSspace TEX_4:def 19 :

registration

let c₁ be non empty TopStruct ;
let c₂ be non empty Subset of c₁;
cluster MaxADSspace a₂ -> non empty strict ;
coherence

proof end;

end;

theorem Th83: :: TEX_4:83

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ holds b₂ is Subset of (MaxADSspace b₂)

proof end;

theorem Th84: :: TEX_4:84

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ holds Sspace b₂ is SubSpace of MaxADSspace b₂

proof end;

theorem Th85: :: TEX_4:85

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds TopStruct(# the carrier of (MaxADSspace b₂),the topology of (MaxADSspace b₂) #) = TopStruct(# the carrier of (MaxADSspace {b₂}),the topology of (MaxADSspace {b₂}) #)

proof end;

theorem Th86: :: TEX_4:86

for b₁ being non empty TopStruct
for b₂, b₃ being non empty Subset of b₁ st b₂ c= b₃ holds
MaxADSspace b₂ is SubSpace of MaxADSspace b₃

proof end;

theorem Th87: :: TEX_4:87

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ holds TopStruct(# the carrier of (MaxADSspace b₂),the topology of (MaxADSspace b₂) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet b₂)),the topology of (MaxADSspace (MaxADSet b₂)) #)

proof end;

theorem Th88: :: TEX_4:88

for b₁ being non empty TopStruct
for b₂, b₃ being non empty Subset of b₁ st b₂ is Subset of (MaxADSspace b₃) holds
MaxADSspace b₂ is SubSpace of MaxADSspace b₃

proof end;

theorem Th89: :: TEX_4:89

for b₁ being non empty TopStruct
for b₂, b₃ being non empty Subset of b₁ holds
( ( b₃ is Subset of (MaxADSspace b₂) & b₂ is Subset of (MaxADSspace b₃) ) iff TopStruct(# the carrier of (MaxADSspace b₂),the topology of (MaxADSspace b₂) #) = TopStruct(# the carrier of (MaxADSspace b₃),the topology of (MaxADSspace b₃) #) )

proof end;

registration

let c₁ be non empty non trivial TopStruct ;
let c₂ be non empty non trivial Subset of c₁;
cluster MaxADSspace a₂ -> non empty non trivial strict ;
coherence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
let c₂ be non empty non proper Subset of c₁;
cluster MaxADSspace a₂ -> non empty strict non proper ;
coherence

proof end;

end;

theorem Th90: :: TEX_4:90

for b₁ being non empty TopSpace
for b₂ being open SubSpace of b₁
for b₃ being non empty Subset of b₁ st b₃ is Subset of b₂ holds
MaxADSspace b₃ is SubSpace of b₂

proof end;

theorem Th91: :: TEX_4:91

for b₁ being non empty TopSpace
for b₂ being closed SubSpace of b₁
for b₃ being non empty Subset of b₁ st b₃ is Subset of b₂ holds
MaxADSspace b₃ is SubSpace of b₂

proof end;