:: Completeness of the Lattices of Domains of a Topological Space
:: by Zbigniew Karno and Toshihiko Watanabe
::
:: Received July 16, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

theorem Th1: :: TDLAT_2:1

for T being TopSpace
for A being Subset of T holds
( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) )

proof end;

theorem Th2: :: TDLAT_2:2

for T being TopSpace
for A being Subset of T holds
( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) )

proof end;

theorem :: TDLAT_2:3

for T being TopSpace
for A, B being Subset of T st B is closed & Cl (Int (A /\ B)) = A holds
A c= B

proof end;

theorem Th4: :: TDLAT_2:4

for T being TopSpace
for A, B being Subset of T st A is open & Int (Cl (A \/ B)) = B holds
A c= B

proof end;

theorem Th5: :: TDLAT_2:5

for T being TopSpace
for A being Subset of T st A c= Cl (Int A) holds
A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A))))

proof end;

theorem Th6: :: TDLAT_2:6

for T being TopSpace
for A being Subset of T st Int (Cl A) c= A holds
Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A))

proof end;

notation

let T be TopSpace;
let F be Subset-Family of T;
synonym Cl F for clf F;

end;

::Properties of the Closure Operation Cl (see also PCOMPS_1).

theorem Th7: :: TDLAT_2:7

for T being TopSpace
for F being Subset-Family of T holds Cl F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) }

proof end;

theorem :: TDLAT_2:8

for T being TopSpace
for F being Subset-Family of T holds Cl F = Cl (Cl F)

proof end;

theorem Th9: :: TDLAT_2:9

for T being TopSpace
for F being Subset-Family of T holds
( F = {} iff Cl F = {} )

proof end;

theorem :: TDLAT_2:10

for T being TopSpace
for F, G being Subset-Family of T holds Cl (F /\ G) c= (Cl F) /\ (Cl G)

proof end;

theorem :: TDLAT_2:11

for T being TopSpace
for F, G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl (F \ G)

proof end;

theorem :: TDLAT_2:12

for T being TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )

proof end;

::for F being Subset-Family of T holds union F c= union(Cl F);
::(see PCOMPS_1:22)

theorem Th13: :: TDLAT_2:13

for T being TopSpace
for F being Subset-Family of T holds meet F c= meet (Cl F)

proof end;

theorem Th14: :: TDLAT_2:14

for T being TopSpace
for F being Subset-Family of T holds Cl (meet F) c= meet (Cl F)

proof end;

theorem Th15: :: TDLAT_2:15

for T being TopSpace
for F being Subset-Family of T holds union (Cl F) c= Cl (union F)

proof end;

definition

let T be TopSpace;
let F be Subset-Family of T;

func Int F -> Subset-Family of T means :Def1: :: TDLAT_2:def 1
for A being Subset of T holds
( A in it iff ex B being Subset of T st
( A = Int B & B in F ) );

existence
ex b₁ being Subset-Family of T st
for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Int B & B in F ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of T st ( for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Int B & B in F ) ) ) & ( for A being Subset of T holds
( A in b₂ iff ex B being Subset of T st
( A = Int B & B in F ) ) ) holds
b₁ = b₂

proof end;

projectivity
for b₁, b₂ being Subset-Family of T st ( for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Int B & B in b₂ ) ) ) holds
for A being Subset of T holds
( A in b₁ iff ex B being Subset of T st
( A = Int B & B in b₁ ) )

proof end;

end;

:: deftheorem Def1 defines Int TDLAT_2:def 1 :
for T being TopSpace
for F, b₃ being Subset-Family of T holds
( b₃ = Int F iff for A being Subset of T holds
( A in b₃ iff ex B being Subset of T st
( A = Int B & B in F ) ) );

::Properties of the Interior Operation Int.

theorem Th16: :: TDLAT_2:16

for T being TopSpace
for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) }

proof end;

theorem :: TDLAT_2:17

canceled;

::$CT

theorem Th17: :: TDLAT_2:18

for T being TopSpace
for F being Subset-Family of T holds Int F is open

proof end;

theorem Th18: :: TDLAT_2:19

for T being TopSpace
for F being Subset-Family of T holds
( F = {} iff Int F = {} )

proof end;

theorem Th19: :: TDLAT_2:20

for T being TopSpace
for A being Subset of T
for F being Subset-Family of T st F = {A} holds
Int F = {(Int A)}

proof end;

theorem :: TDLAT_2:21

for T being TopSpace
for F, G being Subset-Family of T st F c= G holds
Int F c= Int G

proof end;

theorem Th21: :: TDLAT_2:22

for T being TopSpace
for F, G being Subset-Family of T holds Int (F \/ G) = (Int F) \/ (Int G)

proof end;

theorem :: TDLAT_2:23

for T being TopSpace
for F, G being Subset-Family of T holds Int (F /\ G) c= (Int F) /\ (Int G)

proof end;

theorem :: TDLAT_2:24

for T being TopSpace
for F, G being Subset-Family of T holds (Int F) \ (Int G) c= Int (F \ G)

proof end;

theorem :: TDLAT_2:25

for T being TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
( Int A c= union (Int F) & meet (Int F) c= Int A )

proof end;

theorem Th25: :: TDLAT_2:26

for T being TopSpace
for F being Subset-Family of T holds union (Int F) c= union F

proof end;

theorem :: TDLAT_2:27

for T being TopSpace
for F being Subset-Family of T holds meet (Int F) c= meet F

proof end;

theorem Th27: :: TDLAT_2:28

for T being TopSpace
for F being Subset-Family of T holds union (Int F) c= Int (union F)

proof end;

theorem Th28: :: TDLAT_2:29

for T being TopSpace
for F being Subset-Family of T holds Int (meet F) c= meet (Int F)

proof end;

theorem :: TDLAT_2:30

for T being TopSpace
for F being Subset-Family of T st F is finite holds
Int (meet F) = meet (Int F)

proof end;

theorem Th30: :: TDLAT_2:31

for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) }

proof end;

theorem Th31: :: TDLAT_2:32

for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl B) & B in F ) }

proof end;

theorem Th32: :: TDLAT_2:33

for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) }

proof end;

theorem Th33: :: TDLAT_2:34

for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) }

proof end;

theorem :: TDLAT_2:35

for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F)

proof end;

theorem :: TDLAT_2:36

for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (Int (Cl F))) = Int (Cl F)

proof end;

theorem :: TDLAT_2:37

for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:38

for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int (Cl F)) c= meet (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:39

for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int F)) c= union (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:40

for T being non empty TopSpace
for F being Subset-Family of T holds meet (Cl (Int F)) c= meet (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:41

for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Int (Cl F))

proof end;

theorem :: TDLAT_2:42

for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F))

proof end;

theorem :: TDLAT_2:43

for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Cl (Int F))

proof end;

theorem :: TDLAT_2:44

for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Cl (Int F))

proof end;

theorem :: TDLAT_2:45

for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F)

proof end;

theorem :: TDLAT_2:46

for T being non empty TopSpace
for F being Subset-Family of T holds meet (Cl (Int (Cl F))) c= meet (Cl F)

proof end;

theorem :: TDLAT_2:47

for T being non empty TopSpace
for F being Subset-Family of T holds union (Int F) c= union (Int (Cl (Int F)))

proof end;

theorem :: TDLAT_2:48

for T being non empty TopSpace
for F being Subset-Family of T holds meet (Int F) c= meet (Int (Cl (Int F)))

proof end;

theorem Th48: :: TDLAT_2:49

for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F))

proof end;

theorem Th49: :: TDLAT_2:50

for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (meet F)) c= meet (Cl (Int F))

proof end;

theorem Th50: :: TDLAT_2:51

for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl F)) c= Int (Cl (union F))

proof end;

theorem Th51: :: TDLAT_2:52

for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (meet F)) c= meet (Int (Cl F))

proof end;

theorem :: TDLAT_2:53

for T being non empty TopSpace
for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F)))

proof end;

theorem :: TDLAT_2:54

for T being non empty TopSpace
for F being Subset-Family of T holds Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F)))

proof end;

theorem :: TDLAT_2:55

for T being non empty TopSpace
for F being Subset-Family of T holds union (Int (Cl (Int F))) c= Int (Cl (Int (union F)))

proof end;

theorem :: TDLAT_2:56

for T being non empty TopSpace
for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))

proof end;

theorem Th56: :: TDLAT_2:57

for T being non empty TopSpace
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A c= Cl (Int A) ) holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

proof end;

theorem Th57: :: TDLAT_2:58

for T being non empty TopSpace
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
Int (Cl A) c= A ) holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )

proof end;

theorem Th58: :: TDLAT_2:59

for T being non empty TopSpace
for A, B being Subset of T st B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )

proof end;

theorem :: TDLAT_2:60

for T being non empty TopSpace
for A, B being Subset of T st A is condensed holds
( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B )

proof end;

theorem :: TDLAT_2:61

for T being non empty TopSpace
for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds
( Int A c= Int B iff A c= B )

proof end;

theorem :: TDLAT_2:62

for T being non empty TopSpace
for A, B being Subset of T st A is open_condensed & B is open_condensed holds
( Cl A c= Cl B iff A c= B )

proof end;

theorem :: TDLAT_2:63

for T being non empty TopSpace
for A, B being Subset of T st A is closed_condensed & A c= B holds
Cl (Int (A /\ B)) = A

proof end;

theorem Th63: :: TDLAT_2:64

for T being non empty TopSpace
for A, B being Subset of T st B is open_condensed & A c= B holds
Int (Cl (A \/ B)) = B

proof end;

definition

let T be non empty TopSpace;
let IT be Subset-Family of T;

attr IT is domains-family means :: TDLAT_2:def 2
for A being Subset of T st A in IT holds
A is condensed ;

end;

:: deftheorem defines domains-family TDLAT_2:def 2 :
for T being non empty TopSpace
for IT being Subset-Family of T holds
( IT is domains-family iff for A being Subset of T st A in IT holds
A is condensed );

theorem Th64: :: TDLAT_2:65

for T being non empty TopSpace
for F being Subset-Family of T holds
( F c= Domains_of T iff F is domains-family )

proof end;

theorem Th65: :: TDLAT_2:66

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

proof end;

theorem Th66: :: TDLAT_2:67

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )

proof end;

theorem Th67: :: TDLAT_2:68

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
(union F) \/ (Int (Cl (union F))) is condensed

proof end;

theorem Th68: :: TDLAT_2:69

for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
(union F) \/ (Int (Cl (union F))) c= A ) )

proof end;

theorem Th69: :: TDLAT_2:70

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
(meet F) /\ (Cl (Int (meet F))) is condensed

proof end;

theorem Th70: :: TDLAT_2:71

for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
(meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F))) ) )

proof end;

definition

let T be non empty TopSpace;
let IT be Subset-Family of T;

attr IT is closed-domains-family means :: TDLAT_2:def 3
for A being Subset of T st A in IT holds
A is closed_condensed ;

end;

:: deftheorem defines closed-domains-family TDLAT_2:def 3 :
for T being non empty TopSpace
for IT being Subset-Family of T holds
( IT is closed-domains-family iff for A being Subset of T st A in IT holds
A is closed_condensed );

theorem Th71: :: TDLAT_2:72

for T being non empty TopSpace
for F being Subset-Family of T holds
( F c= Closed_Domains_of T iff F is closed-domains-family )

proof end;

theorem Th72: :: TDLAT_2:73

for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
F is domains-family

proof end;

theorem Th73: :: TDLAT_2:74

for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
F is closed

proof end;

theorem :: TDLAT_2:75

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
Cl F is closed-domains-family

proof end;

theorem Th75: :: TDLAT_2:76

for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )

proof end;

theorem Th76: :: TDLAT_2:77

for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Cl (union F) c= A ) )

proof end;

theorem Th77: :: TDLAT_2:78

for T being non empty TopSpace
for F being Subset-Family of T holds
( ( F is closed implies for B being Subset of T st B in F holds
Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Cl (Int (meet F)) ) )

proof end;

definition

let T be non empty TopSpace;
let IT be Subset-Family of T;

attr IT is open-domains-family means :: TDLAT_2:def 4
for A being Subset of T st A in IT holds
A is open_condensed ;

end;

:: deftheorem defines open-domains-family TDLAT_2:def 4 :
for T being non empty TopSpace
for IT being Subset-Family of T holds
( IT is open-domains-family iff for A being Subset of T st A in IT holds
A is open_condensed );

theorem Th78: :: TDLAT_2:79

for T being non empty TopSpace
for F being Subset-Family of T holds
( F c= Open_Domains_of T iff F is open-domains-family )

proof end;

theorem Th79: :: TDLAT_2:80

for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
F is domains-family

proof end;

theorem Th80: :: TDLAT_2:81

for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
F is open

proof end;

theorem :: TDLAT_2:82

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
Int F is open-domains-family

proof end;

theorem Th82: :: TDLAT_2:83

for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )

proof end;

theorem Th83: :: TDLAT_2:84

for T being non empty TopSpace
for F being Subset-Family of T holds
( ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A ) )

proof end;

theorem Th84: :: TDLAT_2:85

for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) )

proof end;

theorem Th85: :: TDLAT_2:86

for T being non empty TopSpace holds the carrier of (Domains_Lattice T) = Domains_of T

proof end;

theorem Th86: :: TDLAT_2:87

for T being non empty TopSpace
for a, b being Element of (Domains_Lattice T)
for A, B being Element of Domains_of T st a = A & b = B holds
( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) )

proof end;

theorem :: TDLAT_2:88

for T being non empty TopSpace holds
( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T )

proof end;

theorem Th88: :: TDLAT_2:89

for T being non empty TopSpace
for a, b being Element of (Domains_Lattice T)
for A, B being Element of Domains_of T st a = A & b = B holds
( a [= b iff A c= B )

proof end;

theorem Th89: :: TDLAT_2:90

for T being non empty TopSpace
for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )

proof end;

theorem Th90: :: TDLAT_2:91

for T being non empty TopSpace holds Domains_Lattice T is complete

proof end;

theorem Th91: :: TDLAT_2:92

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F)))

proof end;

theorem Th92: :: TDLAT_2:93

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )

proof end;

::The Lattice of Closed Domains.

theorem Th93: :: TDLAT_2:94

for T being non empty TopSpace holds the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T

proof end;

theorem Th94: :: TDLAT_2:95

for T being non empty TopSpace
for a, b being Element of (Closed_Domains_Lattice T)
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )

proof end;

theorem :: TDLAT_2:96

for T being non empty TopSpace holds
( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T )

proof end;

theorem Th96: :: TDLAT_2:97

for T being non empty TopSpace
for a, b being Element of (Closed_Domains_Lattice T)
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )

proof end;

theorem Th97: :: TDLAT_2:98

for T being non empty TopSpace
for X being Subset of (Closed_Domains_Lattice T) ex a being Element of (Closed_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds
a [= b ) )

proof end;

theorem Th98: :: TDLAT_2:99

for T being non empty TopSpace holds Closed_Domains_Lattice T is complete

proof end;

theorem :: TDLAT_2:100

for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)

proof end;

theorem :: TDLAT_2:101

for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )

proof end;

theorem :: TDLAT_2:102

for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )

proof end;

::The Lattice of Open Domains.

theorem Th102: :: TDLAT_2:103

for T being non empty TopSpace holds the carrier of (Open_Domains_Lattice T) = Open_Domains_of T

proof end;

theorem Th103: :: TDLAT_2:104

for T being non empty TopSpace
for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )

proof end;

theorem :: TDLAT_2:105

for T being non empty TopSpace holds
( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T )

proof end;

theorem Th105: :: TDLAT_2:106

for T being non empty TopSpace
for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )

proof end;

theorem Th106: :: TDLAT_2:107

for T being non empty TopSpace
for X being Subset of (Open_Domains_Lattice T) ex a being Element of (Open_Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b ) )

proof end;

theorem Th107: :: TDLAT_2:108

for T being non empty TopSpace holds Open_Domains_Lattice T is complete

proof end;

theorem :: TDLAT_2:109

for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Open_Domains_Lattice T) st X = F holds
"\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F))

proof end;

theorem :: TDLAT_2:110

for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Open_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) )

proof end;

theorem :: TDLAT_2:111

for T being non empty TopSpace
for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))

proof end;