:: TDLAT_1  semantic presentation begin  



theorem :: TDLAT_1:1 (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))) "iff" (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "B")))  ")" ))) ; 
 
theorem :: TDLAT_1:2 (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))) "iff" (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ))  ")" ))) ; 
 



theorem :: TDLAT_1:3 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))))) ; 
 
theorem :: TDLAT_1:4 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")) ")" ) ")" ))))) ; 
 
theorem :: TDLAT_1:5 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: TDLAT_1:6 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "or" (Bool (Set (Var "B")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "B")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ))))) ; 
 
theorem :: TDLAT_1:7 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  ) "or" (Bool (Set (Var "B")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "B")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ))))) ; 
 
theorem :: TDLAT_1:8 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T")))))) ; 
 
theorem :: TDLAT_1:9 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))))) ; 
 
theorem :: TDLAT_1:10 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "B")) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "B")) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: TDLAT_1:11 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: TDLAT_1:12 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "B")) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "B")) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: TDLAT_1:13 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")) ")" ))))) ; 
 begin  
theorem :: TDLAT_1:14 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T"))) "is"   ($#v4_tops_1 :::"condensed"::: )  )) ; 
 
theorem :: TDLAT_1:15 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))) "is"   ($#v4_tops_1 :::"condensed"::: )  )) ; 
 
theorem :: TDLAT_1:16 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  )) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v4_tops_1 :::"condensed"::: )  ))) ; 
 
theorem :: TDLAT_1:17 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v4_tops_1 :::"condensed"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )) "is"   ($#v4_tops_1 :::"condensed"::: )  ) & (Bool (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )) "is"   ($#v4_tops_1 :::"condensed"::: )  )  ")" ))) ; 
 
theorem :: TDLAT_1:18 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T"))) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  )) ; 
 
theorem :: TDLAT_1:19 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  )) ; 
 
theorem :: TDLAT_1:20 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T"))) "is"   ($#v6_tops_1 :::"open_condensed"::: )  )) ; 
 
theorem :: TDLAT_1:21 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))) "is"   ($#v6_tops_1 :::"open_condensed"::: )  )) ; 
 
theorem :: TDLAT_1:22 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")) ")" )) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  ))) ; 
 
theorem :: TDLAT_1:23 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" )) "is"   ($#v6_tops_1 :::"open_condensed"::: )  ))) ; 
 
theorem :: TDLAT_1:24 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  )) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A"))) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  ))) ; 
 
theorem :: TDLAT_1:25 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  )) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A"))) "is"   ($#v6_tops_1 :::"open_condensed"::: )  ))) ; 
 
theorem :: TDLAT_1:26 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  )) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  ))) ; 
 
theorem :: TDLAT_1:27 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  )) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )) "is"   ($#v6_tops_1 :::"open_condensed"::: )  ))) ; 
 
theorem :: TDLAT_1:28 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  ) & (Bool (Set (Var "C")) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  )) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "B"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")) ")" ) ")" ))))) ; 
 
theorem :: TDLAT_1:29 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v6_tops_1 :::"open_condensed"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v6_tops_1 :::"open_condensed"::: )  ) & (Bool (Set (Var "C")) "is"   ($#v6_tops_1 :::"open_condensed"::: )  )) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "B"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "C")) ")" ) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "C")) ")" ) ")" ))))) ; 
 begin  definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"Domains_of"::: "T" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: TDLAT_1:def 1  "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"Domains_of"::: TDLAT_1:def 1 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "A")) "is"   ($#v4_tops_1 :::"condensed"::: )  )  "}"  )); 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  "T") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Domains_Union"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_tdlat_1 :::"Domains_of"::: )  "T" ")" ) means :: TDLAT_1:def 2 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )))); end; 





:: deftheorem    defines :::"Domains_Union"::: TDLAT_1:def 2 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_tdlat_1 :::"Domains_Union"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"D-Union"::: "T" for  :::"Domains_Union"::: "T"; end; definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Domains_Meet"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_tdlat_1 :::"Domains_of"::: )  "T" ")" ) means :: TDLAT_1:def 3 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )))); end; 





:: deftheorem    defines :::"Domains_Meet"::: TDLAT_1:def 3 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tdlat_1 :::"Domains_Meet"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"D-Meet"::: "T" for  :::"Domains_Meet"::: "T"; end; 
theorem :: TDLAT_1:30 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k2_tdlat_1 :::"D-Union"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k3_tdlat_1 :::"D-Meet"::: )  (Set (Var "T")) ")" ) "#)" ) "is"   ($#l3_lattices :::"C_Lattice":::))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Domains_Lattice"::: "T" ->   ($#l3_lattices :::"C_Lattice":::) equals :: TDLAT_1:def 4 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_tdlat_1 :::"Domains_of"::: )  "T" ")" ) "," (Set  "("  ($#k2_tdlat_1 :::"Domains_Union"::: )  "T" ")" ) "," (Set  "("  ($#k3_tdlat_1 :::"Domains_Meet"::: )  "T" ")" ) "#)" ); end; 





:: deftheorem    defines :::"Domains_Lattice"::: TDLAT_1:def 4 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k4_tdlat_1 :::"Domains_Lattice"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k2_tdlat_1 :::"Domains_Union"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k3_tdlat_1 :::"Domains_Meet"::: )  (Set (Var "T")) ")" ) "#)" ))); 
 begin  definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"Closed_Domains_of"::: "T" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: TDLAT_1:def 5  "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "A")) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"Closed_Domains_of"::: TDLAT_1:def 5 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "A")) "is"   ($#v5_tops_1 :::"closed_condensed"::: )  )  "}"  )); 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  "T") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: TDLAT_1:31 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T"))))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Closed_Domains_Union"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  "T" ")" ) means :: TDLAT_1:def 6 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B"))))); end; 





:: deftheorem    defines :::"Closed_Domains_Union"::: TDLAT_1:def 6 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_tdlat_1 :::"Closed_Domains_Union"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"CLD-Union"::: "T" for  :::"Closed_Domains_Union"::: "T"; end; 
theorem :: TDLAT_1:32 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set  "("  ($#k6_tdlat_1 :::"CLD-Union"::: )  (Set (Var "T")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_tdlat_1 :::"D-Union"::: )  (Set (Var "T")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Closed_Domains_Meet"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  "T" ")" ) means :: TDLAT_1:def 7 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" )))); end; 





:: deftheorem    defines :::"Closed_Domains_Meet"::: TDLAT_1:def 7 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_tdlat_1 :::"Closed_Domains_Meet"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" ) ")" ))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"CLD-Meet"::: "T" for  :::"Closed_Domains_Meet"::: "T"; end; 
theorem :: TDLAT_1:33 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set  "("  ($#k7_tdlat_1 :::"CLD-Meet"::: )  (Set (Var "T")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_tdlat_1 :::"D-Meet"::: )  (Set (Var "T")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; 
 
theorem :: TDLAT_1:34 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k6_tdlat_1 :::"CLD-Union"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k7_tdlat_1 :::"CLD-Meet"::: )  (Set (Var "T")) ")" ) "#)" ) "is"   ($#l3_lattices :::"B_Lattice":::))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Closed_Domains_Lattice"::: "T" ->   ($#l3_lattices :::"B_Lattice":::) equals :: TDLAT_1:def 8 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  "T" ")" ) "," (Set  "("  ($#k6_tdlat_1 :::"Closed_Domains_Union"::: )  "T" ")" ) "," (Set  "("  ($#k7_tdlat_1 :::"Closed_Domains_Meet"::: )  "T" ")" ) "#)" ); end; 





:: deftheorem    defines :::"Closed_Domains_Lattice"::: TDLAT_1:def 8 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k8_tdlat_1 :::"Closed_Domains_Lattice"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k6_tdlat_1 :::"Closed_Domains_Union"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k7_tdlat_1 :::"Closed_Domains_Meet"::: )  (Set (Var "T")) ")" ) "#)" ))); 
 begin  definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"Open_Domains_of"::: "T" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: TDLAT_1:def 9  "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool (Set (Var "A")) "is"   ($#v6_tops_1 :::"open_condensed"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"Open_Domains_of"::: TDLAT_1:def 9 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "A")) "is"   ($#v6_tops_1 :::"open_condensed"::: )  )  "}"  )); 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  "T") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: TDLAT_1:35 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_tdlat_1 :::"Domains_of"::: )  (Set (Var "T"))))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Open_Domains_Union"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  "T" ")" ) means :: TDLAT_1:def 10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" )))); end; 





:: deftheorem    defines :::"Open_Domains_Union"::: TDLAT_1:def 10 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_tdlat_1 :::"Open_Domains_Union"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ) ")" ))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"OPD-Union"::: "T" for  :::"Open_Domains_Union"::: "T"; end; 
theorem :: TDLAT_1:36 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set  "("  ($#k10_tdlat_1 :::"OPD-Union"::: )  (Set (Var "T")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_tdlat_1 :::"D-Union"::: )  (Set (Var "T")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Open_Domains_Meet"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  "T" ")" ) means :: TDLAT_1:def 11 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B"))))); end; 





:: deftheorem    defines :::"Open_Domains_Meet"::: TDLAT_1:def 11 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_tdlat_1 :::"Open_Domains_Meet"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"OPD-Meet"::: "T" for  :::"Open_Domains_Meet"::: "T"; end; 
theorem :: TDLAT_1:37 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set  "("  ($#k11_tdlat_1 :::"OPD-Meet"::: )  (Set (Var "T")) ")" )  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_tdlat_1 :::"D-Meet"::: )  (Set (Var "T")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; 
 
theorem :: TDLAT_1:38 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k10_tdlat_1 :::"OPD-Union"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k11_tdlat_1 :::"OPD-Meet"::: )  (Set (Var "T")) ")" ) "#)" ) "is"   ($#l3_lattices :::"B_Lattice":::))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Open_Domains_Lattice"::: "T" ->   ($#l3_lattices :::"B_Lattice":::) equals :: TDLAT_1:def 12 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  "T" ")" ) "," (Set  "("  ($#k10_tdlat_1 :::"Open_Domains_Union"::: )  "T" ")" ) "," (Set  "("  ($#k11_tdlat_1 :::"Open_Domains_Meet"::: )  "T" ")" ) "#)" ); end; 





:: deftheorem    defines :::"Open_Domains_Lattice"::: TDLAT_1:def 12 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k12_tdlat_1 :::"Open_Domains_Lattice"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k10_tdlat_1 :::"Open_Domains_Union"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k11_tdlat_1 :::"Open_Domains_Meet"::: )  (Set (Var "T")) ")" ) "#)" ))); 
 begin  
theorem :: TDLAT_1:39 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k6_tdlat_1 :::"CLD-Union"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_tdlat_1 :::"D-Union"::: )  (Set (Var "T")) ")" )  ($#k1_realset1 :::"||"::: )  (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")) ")" )))) ; 
 
theorem :: TDLAT_1:40 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k7_tdlat_1 :::"CLD-Meet"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_tdlat_1 :::"D-Meet"::: )  (Set (Var "T")) ")" )  ($#k1_realset1 :::"||"::: )  (Set  "("  ($#k5_tdlat_1 :::"Closed_Domains_of"::: )  (Set (Var "T")) ")" )))) ; 
 
theorem :: TDLAT_1:41 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k8_tdlat_1 :::"Closed_Domains_Lattice"::: )  (Set (Var "T"))) "is"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set   ($#k4_tdlat_1 :::"Domains_Lattice"::: )  (Set (Var "T"))))) ; 
 
theorem :: TDLAT_1:42 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k10_tdlat_1 :::"OPD-Union"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_tdlat_1 :::"D-Union"::: )  (Set (Var "T")) ")" )  ($#k1_realset1 :::"||"::: )  (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")) ")" )))) ; 
 
theorem :: TDLAT_1:43 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k11_tdlat_1 :::"OPD-Meet"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_tdlat_1 :::"D-Meet"::: )  (Set (Var "T")) ")" )  ($#k1_realset1 :::"||"::: )  (Set  "("  ($#k9_tdlat_1 :::"Open_Domains_of"::: )  (Set (Var "T")) ")" )))) ; 
 
theorem :: TDLAT_1:44 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k12_tdlat_1 :::"Open_Domains_Lattice"::: )  (Set (Var "T"))) "is"    ($#m2_nat_lat :::"SubLattice"::: )   "of" (Set   ($#k4_tdlat_1 :::"Domains_Lattice"::: )  (Set (Var "T"))))) ;