:: TDLAT_2 semantic presentation

theorem Th1: :: TDLAT_2:1
for b1 being TopSpace
for b2 being Subset of b1 holds
( Int (Cl (Int b2)) c= Int (Cl b2) & Int (Cl (Int b2)) c= Cl (Int b2) )
proof end;

theorem Th2: :: TDLAT_2:2
for b1 being TopSpace
for b2 being Subset of b1 holds
( Cl (Int b2) c= Cl (Int (Cl b2)) & Int (Cl b2) c= Cl (Int (Cl b2)) )
proof end;

theorem Th3: :: TDLAT_2:3
for b1 being TopSpace
for b2, b3 being Subset of b1 st b3 is closed & Cl (Int (b2 /\ b3)) = b2 holds
b2 c= b3
proof end;

theorem Th4: :: TDLAT_2:4
for b1 being TopSpace
for b2, b3 being Subset of b1 st b2 is open & Int (Cl (b2 \/ b3)) = b3 holds
b2 c= b3
proof end;

theorem Th5: :: TDLAT_2:5
for b1 being TopSpace
for b2 being Subset of b1 st b2 c= Cl (Int b2) holds
b2 \/ (Int (Cl b2)) c= Cl (Int (b2 \/ (Int (Cl b2))))
proof end;

theorem Th6: :: TDLAT_2:6
for b1 being TopSpace
for b2 being Subset of b1 st Int (Cl b2) c= b2 holds
Int (Cl (b2 /\ (Cl (Int b2)))) c= b2 /\ (Cl (Int b2))
proof end;

notation
let c1 be TopSpace;
let c2 be Subset-Family of c1;
synonym Cl c2 for clf c2;
end;

theorem Th7: :: TDLAT_2:7
for b1 being TopSpace
for b2 being Subset-Family of b1 holds Cl b2 = { b3 where B is Subset of b1 : ex b1 being Subset of b1 st
( b3 = Cl b4 & b4 in b2 )
}
proof end;

theorem Th8: :: TDLAT_2:8
for b1 being TopSpace
for b2 being Subset-Family of b1 holds Cl b2 = Cl (Cl b2)
proof end;

theorem Th9: :: TDLAT_2:9
for b1 being TopSpace
for b2 being Subset-Family of b1 holds
( b2 = {} iff Cl b2 = {} )
proof end;

theorem Th10: :: TDLAT_2:10
for b1 being TopSpace
for b2, b3 being Subset-Family of b1 holds Cl (b2 /\ b3) c= (Cl b2) /\ (Cl b3)
proof end;

theorem Th11: :: TDLAT_2:11
for b1 being TopSpace
for b2, b3 being Subset-Family of b1 holds (Cl b2) \ (Cl b3) c= Cl (b2 \ b3)
proof end;

theorem Th12: :: TDLAT_2:12
for b1 being TopSpace
for b2 being Subset-Family of b1
for b3 being Subset of b1 st b3 in b2 holds
( meet (Cl b2) c= Cl b3 & Cl b3 c= union (Cl b2) )
proof end;

theorem Th13: :: TDLAT_2:13
for b1 being TopSpace
for b2 being Subset-Family of b1 holds meet b2 c= meet (Cl b2)
proof end;

theorem Th14: :: TDLAT_2:14
for b1 being TopSpace
for b2 being Subset-Family of b1 holds Cl (meet b2) c= meet (Cl b2)
proof end;

theorem Th15: :: TDLAT_2:15
for b1 being TopSpace
for b2 being Subset-Family of b1 holds union (Cl b2) c= Cl (union b2)
proof end;

definition
let c1 be TopSpace;
let c2 be Subset-Family of c1;
func Int c2 -> Subset-Family of a1 means :Def1: :: TDLAT_2:def 1
for b1 being Subset of a1 holds
( b1 in a3 iff ex b2 being Subset of a1 st
( b1 = Int b2 & b2 in a2 ) );
existence
ex b1 being Subset-Family of c1 st
for b2 being Subset of c1 holds
( b2 in b1 iff ex b3 being Subset of c1 st
( b2 = Int b3 & b3 in c2 ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of c1 st ( for b3 being Subset of c1 holds
( b3 in b1 iff ex b4 being Subset of c1 st
( b3 = Int b4 & b4 in c2 ) ) ) & ( for b3 being Subset of c1 holds
( b3 in b2 iff ex b4 being Subset of c1 st
( b3 = Int b4 & b4 in c2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Int TDLAT_2:def 1 :
for b1 being TopSpace
for b2, b3 being Subset-Family of b1 holds
( b3 = Int b2 iff for b4 being Subset of b1 holds
( b4 in b3 iff ex b5 being Subset of b1 st
( b4 = Int b5 & b5 in b2 ) ) );

theorem Th16: :: TDLAT_2:16
for b1 being TopSpace
for b2 being Subset-Family of b1 holds Int b2 = { b3 where B is Subset of b1 : ex b1 being Subset of b1 st
( b3 = Int b4 & b4 in b2 )
}
proof end;

theorem Th17: :: TDLAT_2:17
for b1 being TopSpace
for b2 being Subset-Family of b1 holds Int b2 = Int (Int b2)
proof end;

theorem Th18: :: TDLAT_2:18
for b1 being TopSpace
for b2 being Subset-Family of b1 holds Int b2 is open
proof end;

theorem Th19: :: TDLAT_2:19
for b1 being TopSpace
for b2 being Subset-Family of b1 holds
( b2 = {} iff Int b2 = {} )
proof end;

theorem Th20: :: TDLAT_2:20
for b1 being TopSpace
for b2 being Subset of b1
for b3 being Subset-Family of b1 st b3 = {b2} holds
Int b3 = {(Int b2)}
proof end;

theorem Th21: :: TDLAT_2:21
for b1 being TopSpace
for b2, b3 being Subset-Family of b1 st b2 c= b3 holds
Int b2 c= Int b3
proof end;

theorem Th22: :: TDLAT_2:22
for b1 being TopSpace
for b2, b3 being Subset-Family of b1 holds Int (b2 \/ b3) = (Int b2) \/ (Int b3)
proof end;

theorem Th23: :: TDLAT_2:23
for b1 being TopSpace
for b2, b3 being Subset-Family of b1 holds Int (b2 /\ b3) c= (Int b2) /\ (Int b3)
proof end;

theorem Th24: :: TDLAT_2:24
for b1 being TopSpace
for b2, b3 being Subset-Family of b1 holds (Int b2) \ (Int b3) c= Int (b2 \ b3)
proof end;

theorem Th25: :: TDLAT_2:25
for b1 being TopSpace
for b2 being Subset-Family of b1
for b3 being Subset of b1 st b3 in b2 holds
( Int b3 c= union (Int b2) & meet (Int b2) c= Int b3 )
proof end;

theorem Th26: :: TDLAT_2:26
for b1 being TopSpace
for b2 being Subset-Family of b1 holds union (Int b2) c= union b2
proof end;

theorem Th27: :: TDLAT_2:27
for b1 being TopSpace
for b2 being Subset-Family of b1 holds meet (Int b2) c= meet b2
proof end;

theorem Th28: :: TDLAT_2:28
for b1 being TopSpace
for b2 being Subset-Family of b1 holds union (Int b2) c= Int (union b2)
proof end;

theorem Th29: :: TDLAT_2:29
for b1 being TopSpace
for b2 being Subset-Family of b1 holds Int (meet b2) c= meet (Int b2)
proof end;

theorem Th30: :: TDLAT_2:30
for b1 being TopSpace
for b2 being Subset-Family of b1 st b2 is finite holds
Int (meet b2) = meet (Int b2)
proof end;

theorem Th31: :: TDLAT_2:31
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Cl (Int b2) = { b3 where B is Subset of b1 : ex b1 being Subset of b1 st
( b3 = Cl (Int b4) & b4 in b2 )
}
proof end;

theorem Th32: :: TDLAT_2:32
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Int (Cl b2) = { b3 where B is Subset of b1 : ex b1 being Subset of b1 st
( b3 = Int (Cl b4) & b4 in b2 )
}
proof end;

theorem Th33: :: TDLAT_2:33
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Cl (Int (Cl b2)) = { b3 where B is Subset of b1 : ex b1 being Subset of b1 st
( b3 = Cl (Int (Cl b4)) & b4 in b2 )
}
proof end;

theorem Th34: :: TDLAT_2:34
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Int (Cl (Int b2)) = { b3 where B is Subset of b1 : ex b1 being Subset of b1 st
( b3 = Int (Cl (Int b4)) & b4 in b2 )
}
proof end;

theorem Th35: :: TDLAT_2:35
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Cl (Int (Cl (Int b2))) = Cl (Int b2)
proof end;

theorem Th36: :: TDLAT_2:36
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Int (Cl (Int (Cl b2))) = Int (Cl b2)
proof end;

theorem Th37: :: TDLAT_2:37
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Int (Cl b2)) c= union (Cl (Int (Cl b2)))
proof end;

theorem Th38: :: TDLAT_2:38
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds meet (Int (Cl b2)) c= meet (Cl (Int (Cl b2)))
proof end;

theorem Th39: :: TDLAT_2:39
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Cl (Int b2)) c= union (Cl (Int (Cl b2)))
proof end;

theorem Th40: :: TDLAT_2:40
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds meet (Cl (Int b2)) c= meet (Cl (Int (Cl b2)))
proof end;

theorem Th41: :: TDLAT_2:41
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Int (Cl (Int b2))) c= union (Int (Cl b2))
proof end;

theorem Th42: :: TDLAT_2:42
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds meet (Int (Cl (Int b2))) c= meet (Int (Cl b2))
proof end;

theorem Th43: :: TDLAT_2:43
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Int (Cl (Int b2))) c= union (Cl (Int b2))
proof end;

theorem Th44: :: TDLAT_2:44
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds meet (Int (Cl (Int b2))) c= meet (Cl (Int b2))
proof end;

theorem Th45: :: TDLAT_2:45
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Cl (Int (Cl b2))) c= union (Cl b2)
proof end;

theorem Th46: :: TDLAT_2:46
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds meet (Cl (Int (Cl b2))) c= meet (Cl b2)
proof end;

theorem Th47: :: TDLAT_2:47
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Int b2) c= union (Int (Cl (Int b2)))
proof end;

theorem Th48: :: TDLAT_2:48
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds meet (Int b2) c= meet (Int (Cl (Int b2)))
proof end;

theorem Th49: :: TDLAT_2:49
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Cl (Int b2)) c= Cl (Int (union b2))
proof end;

theorem Th50: :: TDLAT_2:50
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Cl (Int (meet b2)) c= meet (Cl (Int b2))
proof end;

theorem Th51: :: TDLAT_2:51
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Int (Cl b2)) c= Int (Cl (union b2))
proof end;

theorem Th52: :: TDLAT_2:52
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Int (Cl (meet b2)) c= meet (Int (Cl b2))
proof end;

theorem Th53: :: TDLAT_2:53
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Cl (Int (Cl b2))) c= Cl (Int (Cl (union b2)))
proof end;

theorem Th54: :: TDLAT_2:54
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Cl (Int (Cl (meet b2))) c= meet (Cl (Int (Cl b2)))
proof end;

theorem Th55: :: TDLAT_2:55
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds union (Int (Cl (Int b2))) c= Int (Cl (Int (union b2)))
proof end;

theorem Th56: :: TDLAT_2:56
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds Int (Cl (Int (meet b2))) c= meet (Int (Cl (Int b2)))
proof end;

theorem Th57: :: TDLAT_2:57
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st ( for b3 being Subset of b1 st b3 in b2 holds
b3 c= Cl (Int b3) ) holds
( union b2 c= Cl (Int (union b2)) & Cl (union b2) = Cl (Int (Cl (union b2))) )
proof end;

theorem Th58: :: TDLAT_2:58
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st ( for b3 being Subset of b1 st b3 in b2 holds
Int (Cl b3) c= b3 ) holds
( Int (Cl (meet b2)) c= meet b2 & Int (Cl (Int (meet b2))) = Int (meet b2) )
proof end;

theorem Th59: :: TDLAT_2:59
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b3 is condensed holds
( (Int (Cl (b2 \/ b3))) \/ (b2 \/ b3) = b3 iff b2 c= b3 )
proof end;

theorem Th60: :: TDLAT_2:60
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is condensed holds
( (Cl (Int (b2 /\ b3))) /\ (b2 /\ b3) = b2 iff b2 c= b3 )
proof end;

theorem Th61: :: TDLAT_2:61
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is closed_condensed & b3 is closed_condensed holds
( Int b2 c= Int b3 iff b2 c= b3 )
proof end;

theorem Th62: :: TDLAT_2:62
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is open_condensed & b3 is open_condensed holds
( Cl b2 c= Cl b3 iff b2 c= b3 )
proof end;

theorem Th63: :: TDLAT_2:63
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is closed_condensed & b2 c= b3 holds
Cl (Int (b2 /\ b3)) = b2
proof end;

theorem Th64: :: TDLAT_2:64
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b3 is open_condensed & b2 c= b3 holds
Int (Cl (b2 \/ b3)) = b3
proof end;

definition
let c1 be non empty TopSpace;
let c2 be Subset-Family of c1;
attr a2 is domains-family means :Def2: :: TDLAT_2:def 2
for b1 being Subset of a1 st b1 in a2 holds
b1 is condensed;
end;

:: deftheorem Def2 defines domains-family TDLAT_2:def 2 :
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( b2 is domains-family iff for b3 being Subset of b1 st b3 in b2 holds
b3 is condensed );

theorem Th65: :: TDLAT_2:65
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( b2 c= Domains_of b1 iff b2 is domains-family )
proof end;

theorem Th66: :: TDLAT_2:66
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
( union b2 c= Cl (Int (union b2)) & Cl (union b2) = Cl (Int (Cl (union b2))) )
proof end;

theorem Th67: :: TDLAT_2:67
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
( Int (Cl (meet b2)) c= meet b2 & Int (Cl (Int (meet b2))) = Int (meet b2) )
proof end;

theorem Th68: :: TDLAT_2:68
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
(union b2) \/ (Int (Cl (union b2))) is condensed
proof end;

theorem Th69: :: TDLAT_2:69
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( ( for b3 being Subset of b1 st b3 in b2 holds
b3 c= (union b2) \/ (Int (Cl (union b2))) ) & ( for b3 being Subset of b1 st b3 is condensed & ( for b4 being Subset of b1 st b4 in b2 holds
b4 c= b3 ) holds
(union b2) \/ (Int (Cl (union b2))) c= b3 ) )
proof end;

theorem Th70: :: TDLAT_2:70
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
(meet b2) /\ (Cl (Int (meet b2))) is condensed
proof end;

theorem Th71: :: TDLAT_2:71
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( ( for b3 being Subset of b1 st b3 in b2 holds
(meet b2) /\ (Cl (Int (meet b2))) c= b3 ) & ( b2 = {} or for b3 being Subset of b1 st b3 is condensed & ( for b4 being Subset of b1 st b4 in b2 holds
b3 c= b4 ) holds
b3 c= (meet b2) /\ (Cl (Int (meet b2))) ) )
proof end;

definition
let c1 be non empty TopSpace;
let c2 be Subset-Family of c1;
attr a2 is closed-domains-family means :Def3: :: TDLAT_2:def 3
for b1 being Subset of a1 st b1 in a2 holds
b1 is closed_condensed;
end;

:: deftheorem Def3 defines closed-domains-family TDLAT_2:def 3 :
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( b2 is closed-domains-family iff for b3 being Subset of b1 st b3 in b2 holds
b3 is closed_condensed );

theorem Th72: :: TDLAT_2:72
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( b2 c= Closed_Domains_of b1 iff b2 is closed-domains-family )
proof end;

theorem Th73: :: TDLAT_2:73
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is closed-domains-family holds
b2 is domains-family
proof end;

theorem Th74: :: TDLAT_2:74
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is closed-domains-family holds
b2 is closed
proof end;

theorem Th75: :: TDLAT_2:75
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
Cl b2 is closed-domains-family
proof end;

theorem Th76: :: TDLAT_2:76
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is closed-domains-family holds
( Cl (union b2) is closed_condensed & Cl (Int (meet b2)) is closed_condensed )
proof end;

theorem Th77: :: TDLAT_2:77
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( ( for b3 being Subset of b1 st b3 in b2 holds
b3 c= Cl (union b2) ) & ( for b3 being Subset of b1 st b3 is closed_condensed & ( for b4 being Subset of b1 st b4 in b2 holds
b4 c= b3 ) holds
Cl (union b2) c= b3 ) )
proof end;

theorem Th78: :: TDLAT_2:78
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( ( b2 is closed implies for b3 being Subset of b1 st b3 in b2 holds
Cl (Int (meet b2)) c= b3 ) & ( b2 = {} or for b3 being Subset of b1 st b3 is closed_condensed & ( for b4 being Subset of b1 st b4 in b2 holds
b3 c= b4 ) holds
b3 c= Cl (Int (meet b2)) ) )
proof end;

definition
let c1 be non empty TopSpace;
let c2 be Subset-Family of c1;
attr a2 is open-domains-family means :Def4: :: TDLAT_2:def 4
for b1 being Subset of a1 st b1 in a2 holds
b1 is open_condensed;
end;

:: deftheorem Def4 defines open-domains-family TDLAT_2:def 4 :
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( b2 is open-domains-family iff for b3 being Subset of b1 st b3 in b2 holds
b3 is open_condensed );

theorem Th79: :: TDLAT_2:79
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( b2 c= Open_Domains_of b1 iff b2 is open-domains-family )
proof end;

theorem Th80: :: TDLAT_2:80
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is open-domains-family holds
b2 is domains-family
proof end;

theorem Th81: :: TDLAT_2:81
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is open-domains-family holds
b2 is open
proof end;

theorem Th82: :: TDLAT_2:82
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
Int b2 is open-domains-family
proof end;

theorem Th83: :: TDLAT_2:83
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is open-domains-family holds
( Int (meet b2) is open_condensed & Int (Cl (union b2)) is open_condensed )
proof end;

theorem Th84: :: TDLAT_2:84
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( ( b2 is open implies for b3 being Subset of b1 st b3 in b2 holds
b3 c= Int (Cl (union b2)) ) & ( for b3 being Subset of b1 st b3 is open_condensed & ( for b4 being Subset of b1 st b4 in b2 holds
b4 c= b3 ) holds
Int (Cl (union b2)) c= b3 ) )
proof end;

theorem Th85: :: TDLAT_2:85
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 holds
( ( for b3 being Subset of b1 st b3 in b2 holds
Int (meet b2) c= b3 ) & ( b2 = {} or for b3 being Subset of b1 st b3 is open_condensed & ( for b4 being Subset of b1 st b4 in b2 holds
b3 c= b4 ) holds
b3 c= Int (meet b2) ) )
proof end;

theorem Th86: :: TDLAT_2:86
for b1 being non empty TopSpace holds the carrier of (Domains_Lattice b1) = Domains_of b1
proof end;

theorem Th87: :: TDLAT_2:87
for b1 being non empty TopSpace
for b2, b3 being Element of (Domains_Lattice b1)
for b4, b5 being Element of Domains_of b1 st b2 = b4 & b3 = b5 holds
( b2 "\/" b3 = (Int (Cl (b4 \/ b5))) \/ (b4 \/ b5) & b2 "/\" b3 = (Cl (Int (b4 /\ b5))) /\ (b4 /\ b5) )
proof end;

theorem Th88: :: TDLAT_2:88
for b1 being non empty TopSpace holds
( Bottom (Domains_Lattice b1) = {} b1 & Top (Domains_Lattice b1) = [#] b1 )
proof end;

theorem Th89: :: TDLAT_2:89
for b1 being non empty TopSpace
for b2, b3 being Element of (Domains_Lattice b1)
for b4, b5 being Element of Domains_of b1 st b2 = b4 & b3 = b5 holds
( b2 [= b3 iff b4 c= b5 )
proof end;

theorem Th90: :: TDLAT_2:90
for b1 being non empty TopSpace
for b2 being Subset of (Domains_Lattice b1) ex b3 being Element of (Domains_Lattice b1) st
( b2 is_less_than b3 & ( for b4 being Element of (Domains_Lattice b1) st b2 is_less_than b4 holds
b3 [= b4 ) )
proof end;

theorem Th91: :: TDLAT_2:91
for b1 being non empty TopSpace holds Domains_Lattice b1 is complete
proof end;

theorem Th92: :: TDLAT_2:92
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
for b3 being Subset of (Domains_Lattice b1) st b3 = b2 holds
"\/" b3,(Domains_Lattice b1) = (union b2) \/ (Int (Cl (union b2)))
proof end;

theorem Th93: :: TDLAT_2:93
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is domains-family holds
for b3 being Subset of (Domains_Lattice b1) st b3 = b2 holds
( ( b3 <> {} implies "/\" b3,(Domains_Lattice b1) = (meet b2) /\ (Cl (Int (meet b2))) ) & ( b3 = {} implies "/\" b3,(Domains_Lattice b1) = [#] b1 ) )
proof end;

theorem Th94: :: TDLAT_2:94
for b1 being non empty TopSpace holds the carrier of (Closed_Domains_Lattice b1) = Closed_Domains_of b1
proof end;

theorem Th95: :: TDLAT_2:95
for b1 being non empty TopSpace
for b2, b3 being Element of (Closed_Domains_Lattice b1)
for b4, b5 being Element of Closed_Domains_of b1 st b2 = b4 & b3 = b5 holds
( b2 "\/" b3 = b4 \/ b5 & b2 "/\" b3 = Cl (Int (b4 /\ b5)) )
proof end;

theorem Th96: :: TDLAT_2:96
for b1 being non empty TopSpace holds
( Bottom (Closed_Domains_Lattice b1) = {} b1 & Top (Closed_Domains_Lattice b1) = [#] b1 )
proof end;

theorem Th97: :: TDLAT_2:97
for b1 being non empty TopSpace
for b2, b3 being Element of (Closed_Domains_Lattice b1)
for b4, b5 being Element of Closed_Domains_of b1 st b2 = b4 & b3 = b5 holds
( b2 [= b3 iff b4 c= b5 )
proof end;

theorem Th98: :: TDLAT_2:98
for b1 being non empty TopSpace
for b2 being Subset of (Closed_Domains_Lattice b1) ex b3 being Element of (Closed_Domains_Lattice b1) st
( b2 is_less_than b3 & ( for b4 being Element of (Closed_Domains_Lattice b1) st b2 is_less_than b4 holds
b3 [= b4 ) )
proof end;

theorem Th99: :: TDLAT_2:99
for b1 being non empty TopSpace holds Closed_Domains_Lattice b1 is complete
proof end;

theorem Th100: :: TDLAT_2:100
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is closed-domains-family holds
for b3 being Subset of (Closed_Domains_Lattice b1) st b3 = b2 holds
"\/" b3,(Closed_Domains_Lattice b1) = Cl (union b2)
proof end;

theorem Th101: :: TDLAT_2:101
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is closed-domains-family holds
for b3 being Subset of (Closed_Domains_Lattice b1) st b3 = b2 holds
( ( b3 <> {} implies "/\" b3,(Closed_Domains_Lattice b1) = Cl (Int (meet b2)) ) & ( b3 = {} implies "/\" b3,(Closed_Domains_Lattice b1) = [#] b1 ) )
proof end;

theorem Th102: :: TDLAT_2:102
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is closed-domains-family holds
for b3 being Subset of (Domains_Lattice b1) st b3 = b2 holds
( ( b3 <> {} implies "/\" b3,(Domains_Lattice b1) = Cl (Int (meet b2)) ) & ( b3 = {} implies "/\" b3,(Domains_Lattice b1) = [#] b1 ) )
proof end;

theorem Th103: :: TDLAT_2:103
for b1 being non empty TopSpace holds the carrier of (Open_Domains_Lattice b1) = Open_Domains_of b1
proof end;

theorem Th104: :: TDLAT_2:104
for b1 being non empty TopSpace
for b2, b3 being Element of (Open_Domains_Lattice b1)
for b4, b5 being Element of Open_Domains_of b1 st b2 = b4 & b3 = b5 holds
( b2 "\/" b3 = Int (Cl (b4 \/ b5)) & b2 "/\" b3 = b4 /\ b5 )
proof end;

theorem Th105: :: TDLAT_2:105
for b1 being non empty TopSpace holds
( Bottom (Open_Domains_Lattice b1) = {} b1 & Top (Open_Domains_Lattice b1) = [#] b1 )
proof end;

theorem Th106: :: TDLAT_2:106
for b1 being non empty TopSpace
for b2, b3 being Element of (Open_Domains_Lattice b1)
for b4, b5 being Element of Open_Domains_of b1 st b2 = b4 & b3 = b5 holds
( b2 [= b3 iff b4 c= b5 )
proof end;

theorem Th107: :: TDLAT_2:107
for b1 being non empty TopSpace
for b2 being Subset of (Open_Domains_Lattice b1) ex b3 being Element of (Open_Domains_Lattice b1) st
( b2 is_less_than b3 & ( for b4 being Element of (Open_Domains_Lattice b1) st b2 is_less_than b4 holds
b3 [= b4 ) )
proof end;

theorem Th108: :: TDLAT_2:108
for b1 being non empty TopSpace holds Open_Domains_Lattice b1 is complete
proof end;

theorem Th109: :: TDLAT_2:109
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is open-domains-family holds
for b3 being Subset of (Open_Domains_Lattice b1) st b3 = b2 holds
"\/" b3,(Open_Domains_Lattice b1) = Int (Cl (union b2))
proof end;

theorem Th110: :: TDLAT_2:110
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is open-domains-family holds
for b3 being Subset of (Open_Domains_Lattice b1) st b3 = b2 holds
( ( b3 <> {} implies "/\" b3,(Open_Domains_Lattice b1) = Int (meet b2) ) & ( b3 = {} implies "/\" b3,(Open_Domains_Lattice b1) = [#] b1 ) )
proof end;

theorem Th111: :: TDLAT_2:111
for b1 being non empty TopSpace
for b2 being Subset-Family of b1 st b2 is open-domains-family holds
for b3 being Subset of (Domains_Lattice b1) st b3 = b2 holds
"\/" b3,(Domains_Lattice b1) = Int (Cl (union b2))
proof end;