:: LOPCLSET  semantic presentation begin  






definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"OpenClosedSet"::: "T" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: LOPCLSET:def 1  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )  "}"  ; end; 





:: deftheorem    defines :::"OpenClosedSet"::: LOPCLSET:def 1 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )  "}"  )); 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  "T") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: LOPCLSET:1 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))))) "holds"  (Bool (Set (Var "X")) "is"   ($#v3_pre_topc :::"open"::: )  ))) ; 
 
theorem :: LOPCLSET:2 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))))) "holds"  (Bool (Set (Var "X")) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: LOPCLSET:3 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v4_pre_topc :::"closed"::: )  )) "holds"  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")))))) ; 
 



definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "C", "D" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Const "T"))); :: original: :::"\/"::: redefine func "C" :::"\/"::: "D" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  "T"); :: original: :::"/\"::: redefine func "C" :::"/\"::: "D" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  "T"); end; definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"T_join"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  "T" ")" ) means :: LOPCLSET:def 2 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_lopclset :::"\/"::: )  (Set (Var "B"))))); func  :::"T_meet"::: "T" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  "T" ")" ) means :: LOPCLSET:def 3 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  "T") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k3_lopclset :::"/\"::: )  (Set (Var "B"))))); end; 










:: deftheorem    defines :::"T_join"::: LOPCLSET:def 2 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_lopclset :::"T_join"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_lopclset :::"\/"::: )  (Set (Var "B")))))  ")" ))); 
 
:: deftheorem    defines :::"T_meet"::: LOPCLSET:def 3 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_lopclset :::"T_meet"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k3_lopclset :::"/\"::: )  (Set (Var "B")))))  ")" ))); 
 
theorem :: LOPCLSET:4 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k4_lopclset :::"T_join"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k5_lopclset :::"T_meet"::: )  (Set (Var "T")) ")" ) "#)" )  (Bool  "for" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "y9")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_lattices :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x9"))  ($#k2_lopclset :::"\/"::: )  (Set (Var "y9"))))))) ; 
 
theorem :: LOPCLSET:5 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k4_lopclset :::"T_join"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k5_lopclset :::"T_meet"::: )  (Set (Var "T")) ")" ) "#)" )  (Bool  "for" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "y9")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_lattices :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x9"))  ($#k3_lopclset :::"/\"::: )  (Set (Var "y9"))))))) ; 
 
theorem :: LOPCLSET:6 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T"))) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))))) ; 
 
theorem :: LOPCLSET:7 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))))) ; 
 
theorem :: LOPCLSET:8 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_subset_1 :::"`"::: )  ) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")))))) ; 
 
theorem :: LOPCLSET:9 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k4_lopclset :::"T_join"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k5_lopclset :::"T_meet"::: )  (Set (Var "T")) ")" ) "#)" ) "is"   ($#l3_lattices :::"Lattice":::))) ; 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"OpenClosedSetLatt"::: "T" ->   ($#l3_lattices :::"Lattice":::) equals :: LOPCLSET:def 4 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  "T" ")" ) "," (Set  "("  ($#k4_lopclset :::"T_join"::: )  "T" ")" ) "," (Set  "("  ($#k5_lopclset :::"T_meet"::: )  "T" ")" ) "#)" ); end; 





:: deftheorem    defines :::"OpenClosedSetLatt"::: LOPCLSET:def 4 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k4_lopclset :::"T_join"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k5_lopclset :::"T_meet"::: )  (Set (Var "T")) ")" ) "#)" ))); 
 
theorem :: LOPCLSET:10 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set (Var "T")) ")" ) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_lattices :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "y")))))) ; 
 
theorem :: LOPCLSET:11 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set (Var "T")) ")" ) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_lattices :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "y")))))) ; 
 
theorem :: LOPCLSET:12 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set (Var "T")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set (Var "T"))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k6_lopclset :::"OpenClosedSetLatt"::: )  "T") ->   ($#v17_lattices :::"Boolean"::: )   ; 
end; 
theorem :: LOPCLSET:13 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set (Var "T")) ")" ))) ; 
 
theorem :: LOPCLSET:14 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set (Var "T")) ")" ))) ; 
 




registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v4_lattices :::"join-commutative"::: )     ($#v5_lattices :::"join-associative"::: )     ($#v6_lattices :::"meet-commutative"::: )     ($#v7_lattices :::"meet-associative"::: )     ($#v8_lattices :::"meet-absorbing"::: )     ($#v9_lattices :::"join-absorbing"::: )     ($#v10_lattices :::"Lattice-like"::: )     ($#v11_lattices :::"distributive"::: )     ($#v12_lattices :::"modular"::: )     ($#v13_lattices :::"lower-bounded"::: )     ($#v14_lattices :::"upper-bounded"::: )     ($#v15_lattices :::"bounded"::: )     ($#v16_lattices :::"complemented"::: )     ($#v17_lattices :::"Boolean"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end; 
















definitionlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); func  :::"ultraset"::: "BL" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "BL" equals :: LOPCLSET:def 5  "{"  (Set (Var "F")) where F "is"   ($#m1_subset_1 :::"Filter":::) "of" "BL" : (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"ultraset"::: LOPCLSET:def 5 :  (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "F")) where F "is"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL")) : (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  )  "}"  )); 
 registrationlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); 
cluster (Set   ($#k7_lopclset :::"ultraset"::: )  "BL") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: LOPCLSET:15 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")))) "iff" (Bool  "ex" (Set (Var "UF")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL")) "st"  (Bool  "("  (Bool (Set (Var "UF"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "UF")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  )  ")" ))  ")" ))) ; 
 
theorem :: LOPCLSET:16 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds"  (Bool  "{"  (Set (Var "F")) where F "is"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL")) : (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  ) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" )  "}"    ($#r1_tarski :::"c="::: )  (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")))))) ; 
 definitionlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); func  :::"UFilter"::: "BL" ->   ($#m1_hidden :::"Function":::) means :: LOPCLSET:def 6 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "BL")) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "BL" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "UF")) where UF "is"   ($#m1_subset_1 :::"Filter":::) "of" "BL" : (Bool  "("  (Bool (Set (Var "UF")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  ) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "UF")))  ")" )  "}"  )  ")" )  ")" ); end; 





:: deftheorem    defines :::"UFilter"::: LOPCLSET:def 6 :  (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "BL")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "UF")) where UF "is"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL")) : (Bool  "("  (Bool (Set (Var "UF")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  ) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "UF")))  ")" )  "}"  )  ")" )  ")" )  ")" ))); 
 
theorem :: LOPCLSET:17 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))) "iff" (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL")) "st"  (Bool  "("  (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  ) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ))  ")" )))) ; 
 
theorem :: LOPCLSET:18 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL")) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  ) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" )  ")" )))) ; 
 
theorem :: LOPCLSET:19 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) "or" (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" )  ")" )))) ; 
 
theorem :: LOPCLSET:20 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds"  (Bool (Set (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: LOPCLSET:21 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds"  (Bool (Set (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  "("  ($#k8_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ))))) ; 
 definitionlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); :: original: :::"UFilter"::: redefine func  :::"UFilter"::: "BL" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "BL") "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k7_lopclset :::"ultraset"::: )  "BL" ")" ) ")" ); end; definitionlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); func  :::"StoneR"::: "BL" ->    ($#m1_hidden :::"set"::: )   equals :: LOPCLSET:def 7 (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k9_lopclset :::"UFilter"::: )  "BL" ")" )); end; 





:: deftheorem    defines :::"StoneR"::: LOPCLSET:def 7 :  (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set   ($#k10_lopclset :::"StoneR"::: )  (Set (Var "BL")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k9_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )))); 
 registrationlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); 
cluster (Set   ($#k10_lopclset :::"StoneR"::: )  "BL") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: LOPCLSET:22 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set   ($#k10_lopclset :::"StoneR"::: )  (Set (Var "BL")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")) ")" )))) ; 
 
theorem :: LOPCLSET:23 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_lopclset :::"StoneR"::: )  (Set (Var "BL")))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "st" (Bool (Set (Set  "("  ($#k9_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))  ")" ))) ; 
 definitionlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); func  :::"StoneSpace"::: "BL" ->   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) means :: LOPCLSET:def 8 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k7_lopclset :::"ultraset"::: )  "BL")) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "A")) ")" ) where A "is"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k7_lopclset :::"ultraset"::: )  "BL" ")" ) : (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_lopclset :::"StoneR"::: )  "BL"))  "}"  )  ")" ); end; 





:: deftheorem    defines :::"StoneSpace"::: LOPCLSET:def 8 :  (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_lopclset :::"StoneSpace"::: )  (Set (Var "BL")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "A")) ")" ) where A "is"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")) ")" ) : (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_lopclset :::"StoneR"::: )  (Set (Var "BL"))))  "}"  )  ")" )  ")" ))); 
 registrationlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); 
cluster (Set   ($#k11_lopclset :::"StoneSpace"::: )  "BL") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: LOPCLSET:24 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "BL"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  ) & (Bool (Bool  "not" (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k9_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))) "holds"  (Bool  "not" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))))) ; 
 
theorem :: LOPCLSET:25 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds"  (Bool (Set (Set  "("  ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "(" (Set  "("  ($#k9_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k7_lattices :::"`"::: )  ")" ))))) ; 
 definitionlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); func  :::"StoneBLattice"::: "BL" ->   ($#l3_lattices :::"Lattice":::) equals :: LOPCLSET:def 9 (Set   ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set  "("  ($#k11_lopclset :::"StoneSpace"::: )  "BL" ")" )); end; 





:: deftheorem    defines :::"StoneBLattice"::: LOPCLSET:def 9 :  (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set   ($#k12_lopclset :::"StoneBLattice"::: )  (Set (Var "BL")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set  "("  ($#k11_lopclset :::"StoneSpace"::: )  (Set (Var "BL")) ")" )))); 
 registrationlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); 
cluster (Set   ($#k8_lopclset :::"UFilter"::: )  "BL") ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: LOPCLSET:26 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k10_lopclset :::"StoneR"::: )  (Set (Var "BL")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL"))))) ; 
 
theorem :: LOPCLSET:27 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "not" (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "Y")) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  "D"); 
end; 
theorem :: LOPCLSET:28 (Bool  "for" (Set (Var "L")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))  ($#r2_hidden :::"in"::: )  (Set  ($#k3_filter_0 :::"<."::: ) (Set (Var "D")) ($#k3_filter_0 :::".)"::: ) ))) "holds"  (Bool  "ex" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "D"))) & (Bool (Set   ($#k2_lattice4 :::"FinMeet"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))  ")" )))) ; 
 
theorem :: LOPCLSET:29 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "F")) "is"   ($#v1_filter_0 :::"being_ultrafilter"::: )  ) "or"  "not" (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ))) ; 
 
theorem :: LOPCLSET:30 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set (Set  "("  ($#k9_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_lattices :::"Bottom"::: )  (Set (Var "BL")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: LOPCLSET:31 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set (Set  "("  ($#k9_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k6_lattices :::"Top"::: )  (Set (Var "BL")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL"))))) ; 
 
theorem :: LOPCLSET:32 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::)  "st" (Bool (Bool (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))) & (Bool (Set (Var "X")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k10_lopclset :::"StoneR"::: )  (Set (Var "BL")) ")" ))) "holds"  (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "X")) "st" (Bool (Set   ($#k7_lopclset :::"ultraset"::: )  (Set (Var "BL")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "Y"))))))) ; 
 
theorem :: LOPCLSET:33 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set   ($#k10_lopclset :::"StoneR"::: )  (Set (Var "BL")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_lopclset :::"OpenClosedSet"::: )  (Set  "("  ($#k11_lopclset :::"StoneSpace"::: )  (Set (Var "BL")) ")" )))) ; 
 definitionlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); :: original: :::"UFilter"::: redefine func  :::"UFilter"::: "BL" ->    ($#m1_lattice4 :::"Homomorphism"::: )   "of" "BL" "," (Set   ($#k12_lopclset :::"StoneBLattice"::: )  "BL"); end; 
theorem :: LOPCLSET:34 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k13_lopclset :::"UFilter"::: )  (Set (Var "BL")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k12_lopclset :::"StoneBLattice"::: )  (Set (Var "BL")) ")" )))) ; 
 registrationlet "BL" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::); 
cluster (Set   ($#k8_lopclset :::"UFilter"::: )  "BL") ->   ($#v3_funct_2 :::"bijective"::: )    for  ($#m1_subset_1 :::"Function":::) "of" "BL" "," (Set  "("  ($#k12_lopclset :::"StoneBLattice"::: )  "BL" ")" ); 
end; 
theorem :: LOPCLSET:35 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) "holds"  (Bool (Set (Var "BL")) "," (Set   ($#k12_lopclset :::"StoneBLattice"::: )  (Set (Var "BL")))  ($#r1_filter_1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: LOPCLSET:36 (Bool  "for" (Set (Var "BL")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l3_lattices :::"B_Lattice":::) (Bool  "ex" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Set (Var "BL")) "," (Set   ($#k6_lopclset :::"OpenClosedSetLatt"::: )  (Set (Var "T")))  ($#r1_filter_1 :::"are_isomorphic"::: )  ))) ;