:: 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 b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in F ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in F ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of T st
( A = Int B & B in F ) ) ) holds
b1 = b2
proof end;
projectivity
for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in b2 ) ) ) holds
for A being Subset of T holds
( A in b1 iff ex B being Subset of T st
( A = Int B & B in b1 ) )
proof end;
end;

:: deftheorem Def1 defines Int TDLAT_2:def 1 :
for T being TopSpace
for F, b3 being Subset-Family of T holds
( b3 = Int F iff for A being Subset of T holds
( A in b3 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;