:: FILTER_0 semantic presentation begin theorem :: FILTER_0:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "r")) ($#k3_lattices :::""\/""::: ) (Set (Var "p"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "r")) ($#k3_lattices :::""\/""::: ) (Set (Var "q")))))) ; theorem :: FILTER_0:2 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r3_lattices :::"[="::: ) (Set (Var "r"))))) ; theorem :: FILTER_0:3 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "q")) ($#k3_lattices :::""\/""::: ) (Set (Var "r")))))) ; theorem :: FILTER_0:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_lattices :::"[="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "c"))) ($#r1_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k3_lattices :::""\/""::: ) (Set (Var "d")))))) ; theorem :: FILTER_0:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r3_lattices :::"[="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "c"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "d")))))) ; theorem :: FILTER_0:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r3_lattices :::"[="::: ) (Set (Var "c"))))) ; theorem :: FILTER_0:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); mode Filter of "L" is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v19_lattices :::"final"::: ) ($#v20_lattices :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "L"; end; theorem :: FILTER_0:8 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )) ")" ))) ; theorem :: FILTER_0:9 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) ")" ) ")" ))) ; theorem :: FILTER_0:10 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Set (Var "q")) ($#k3_lattices :::""\/""::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) ")" )))) ; theorem :: FILTER_0:11 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"1_Lattice":::))) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "H"))))) ; theorem :: FILTER_0:12 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"1_Lattice":::))) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")))) ; theorem :: FILTER_0:13 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")))) "holds" (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) ))) ; theorem :: FILTER_0:14 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); func :::"<.":::"L":::".)"::: -> ($#m1_subset_1 :::"Filter":::) "of" "L" equals :: FILTER_0:def 1 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"); end; :: deftheorem defines :::"<."::: FILTER_0:def 1 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k1_filter_0 :::"<."::: ) (Set (Var "L")) ($#k1_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))); definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"<.":::"p":::".)"::: -> ($#m1_subset_1 :::"Filter":::) "of" "L" equals :: FILTER_0:def 2 "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "p" ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "}" ; end; :: deftheorem defines :::"<."::: FILTER_0:def 2 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "}" ))); theorem :: FILTER_0:15 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) "iff" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) ")" ))) ; theorem :: FILTER_0:16 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) & (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) & (Bool (Set (Set (Var "q")) ($#k3_lattices :::""\/""::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) ")" ))) ; theorem :: FILTER_0:17 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"0_Lattice":::))) "holds" (Bool (Set ($#k1_filter_0 :::"<."::: ) (Set (Var "L")) ($#k1_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k2_filter_0 :::".)"::: ) ))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); attr "F" is :::"being_ultrafilter"::: means :: FILTER_0:def 3 (Bool "(" (Bool "F" ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool "(" "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" "L" "st" (Bool (Bool "F" ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))) "holds" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ) ")" ); end; :: deftheorem defines :::"being_ultrafilter"::: FILTER_0:def 3 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ) ")" ) ")" ))); theorem :: FILTER_0:18 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) ) ")" )))) ; theorem :: FILTER_0:19 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "r"))) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: FILTER_0:20 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"0_Lattice":::)) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) ) ")" )))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func :::"<.":::"D":::".)"::: -> ($#m1_subset_1 :::"Filter":::) "of" "L" means :: FILTER_0:def 4 (Bool "(" (Bool "D" ($#r1_tarski :::"c="::: ) it) & (Bool "(" "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" "L" "st" (Bool (Bool "D" ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) ")" ); end; :: deftheorem defines :::"<."::: FILTER_0:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D")) ($#k3_filter_0 :::".)"::: ) )) "iff" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) ")" ) ")" )))); theorem :: FILTER_0:21 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "F")) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; theorem :: FILTER_0:22 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_tarski :::"c="::: ) (Set (Var "D2")))) "holds" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D1")) ($#k3_filter_0 :::".)"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D2")) ($#k3_filter_0 :::".)"::: ) )))) ; theorem :: FILTER_0:23 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (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 (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D")) ($#k3_filter_0 :::".)"::: ) ))))) ; theorem :: FILTER_0:24 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (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 (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D")) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) ))))) ; theorem :: FILTER_0:25 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"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 (Var "L")) "is" ($#l3_lattices :::"0_Lattice":::)) & (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D")) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_filter_0 :::"<."::: ) (Set (Var "L")) ($#k1_filter_0 :::".)"::: ) )) & (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D")) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) ")" ))) ; theorem :: FILTER_0:26 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"0_Lattice":::)) & (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_filter_0 :::"<."::: ) (Set (Var "L")) ($#k1_filter_0 :::".)"::: ) )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) ")" ))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); attr "F" is :::"prime"::: means :: FILTER_0:def 5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "F") "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "F") "or" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "F") ")" ) ")" )); end; :: deftheorem defines :::"prime"::: FILTER_0:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_filter_0 :::"prime"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "or" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) ")" )) ")" ))); theorem :: FILTER_0:27 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"B_Lattice":::))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_lattices :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "q")) ")" )) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "r"))) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "r")) ($#r3_lattices :::"[="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_lattices :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "q")))) ")" ) ")" ))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"implicative"::: means :: FILTER_0:def 6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k2_lattices :::""/\""::: ) (Set (Var "r"))) ($#r1_lattices :::"[="::: ) (Set (Var "q"))) & (Bool "(" "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Set (Var "p")) ($#k2_lattices :::""/\""::: ) (Set (Var "r1"))) ($#r1_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "r1")) ($#r1_lattices :::"[="::: ) (Set (Var "r"))) ")" ) ")" ))); end; :: deftheorem defines :::"implicative"::: FILTER_0:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_filter_0 :::"implicative"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k2_lattices :::""/\""::: ) (Set (Var "r"))) ($#r1_lattices :::"[="::: ) (Set (Var "q"))) & (Bool "(" "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k2_lattices :::""/\""::: ) (Set (Var "r1"))) ($#r1_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "r1")) ($#r1_lattices :::"[="::: ) (Set (Var "r"))) ")" ) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#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"::: ) ($#v3_filter_0 :::"implicative"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionmode I_Lattice is ($#v3_filter_0 :::"implicative"::: ) ($#l3_lattices :::"Lattice":::); end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); assume (Bool (Set (Const "L")) "is" ($#l3_lattices :::"I_Lattice":::)) ; func "p" :::"=>"::: "q" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: FILTER_0:def 7 (Bool "(" (Bool (Set "p" ($#k4_lattices :::""/\""::: ) it) ($#r3_lattices :::"[="::: ) "q") & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set "p" ($#k4_lattices :::""/\""::: ) (Set (Var "r"))) ($#r3_lattices :::"[="::: ) "q")) "holds" (Bool (Set (Var "r")) ($#r3_lattices :::"[="::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"=>"::: FILTER_0:def 7 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"I_Lattice":::))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "b4"))) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "r"))) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "r")) ($#r3_lattices :::"[="::: ) (Set (Var "b4"))) ")" ) ")" ) ")" )))); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v3_filter_0 :::"implicative"::: ) -> ($#v14_lattices :::"upper-bounded"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: FILTER_0:28 (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "I")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v3_filter_0 :::"implicative"::: ) -> ($#v11_lattices :::"distributive"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) -> ($#v3_filter_0 :::"implicative"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v3_filter_0 :::"implicative"::: ) -> ($#v11_lattices :::"distributive"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: FILTER_0:29 (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "FI")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "FI"))) & (Bool (Set (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))) "holds" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))))) ; theorem :: FILTER_0:30 (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "FI")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))) "holds" (Bool (Set (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func "D1" :::""/\""::: "D2" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: FILTER_0:def 8 "{" (Set "(" (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q")) ")" ) where p, q "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "D1") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "D2") ")" ) "}" ; end; :: deftheorem defines :::""/\""::: FILTER_0:def 8 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "D1")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q")) ")" ) where p, q "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D2"))) ")" ) "}" ))); registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k5_filter_0 :::""/\""::: ) "D2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: FILTER_0:31 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D2")))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D1")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D2")))) & (Bool (Set (Set (Var "q")) ($#k4_lattices :::""/\""::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D1")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D2")))) ")" )))) ; theorem :: FILTER_0:32 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D1")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D2"))))) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D2"))) ")" ))))) ; theorem :: FILTER_0:33 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "D1")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D2")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D1")))))) ; registrationlet "L" be ($#l3_lattices :::"D_Lattice":::); let "F1", "F2" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); cluster (Set "F1" ($#k5_filter_0 :::""/\""::: ) "F2") -> ($#v19_lattices :::"final"::: ) ($#v20_lattices :::"meet-closed"::: ) ; end; theorem :: FILTER_0:34 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "D1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "D2")) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D1")) ($#k3_filter_0 :::".)"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "D2")) ")" ) ($#k3_filter_0 :::".)"::: ) )) & (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "D1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "D2")) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "D1")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D2")) ($#k3_filter_0 :::".)"::: ) ) ")" ) ($#k3_filter_0 :::".)"::: ) )) ")" ))) ; theorem :: FILTER_0:35 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "H")) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r3_lattices :::"[="::: ) (Set (Var "r"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) ")" )) "}" ))) ; theorem :: FILTER_0:36 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "H")))) & (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "H")))) ")" ))) ; theorem :: FILTER_0:37 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "H")) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "F")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "H")) ")" ) ($#k3_filter_0 :::".)"::: ) )))) ; theorem :: FILTER_0:38 (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "F1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "F2")) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "F2")))))) ; theorem :: FILTER_0:39 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "FB")) "," (Set (Var "HB")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) "holds" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "FB")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "HB")) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "FB")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "HB")))))) ; theorem :: FILTER_0:40 (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "DI")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "DI")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "i")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k3_filter_0 :::".)"::: ) ))) "holds" (Bool (Set (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "DI")) ($#k3_filter_0 :::".)"::: ) ))))) ; theorem :: FILTER_0:41 (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "FI")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI"))) & (Bool (Set (Set (Var "j")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))) "holds" (Bool (Set (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))))) ; theorem :: FILTER_0:42 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set (Var "a")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k7_lattices :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "b")))))) ; theorem :: FILTER_0:43 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) "iff" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k7_lattices :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "B")))) ")" ))) ; theorem :: FILTER_0:44 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "FB")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "FB")) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) ) "iff" (Bool "(" (Bool (Set (Var "FB")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "FB"))) "or" (Bool (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "FB"))) ")" ) ")" ) ")" ) ")" ))) ; theorem :: FILTER_0:45 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "FB")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "FB")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_filter_0 :::"<."::: ) (Set (Var "B")) ($#k1_filter_0 :::".)"::: ) )) & (Bool (Set (Var "FB")) "is" ($#v2_filter_0 :::"prime"::: ) ) ")" ) "iff" (Bool (Set (Var "FB")) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) ) ")" ))) ; theorem :: FILTER_0:46 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "FB")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "FB")) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "FB"))) "iff" (Bool (Bool "not" (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "FB")))) ")" )))) ; theorem :: FILTER_0:47 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "FB")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "FB")) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) ) & (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "FB"))) & (Bool (Bool "not" (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "FB")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "FB")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "FB"))) ")" ) ")" ) ")" )))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); func :::"latt"::: "F" -> ($#l3_lattices :::"Lattice":::) means :: FILTER_0:def 9 (Bool "ex" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" "F" "st" (Bool "(" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) "F")) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) "F")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" "F" "," (Set (Var "o1")) "," (Set (Var "o2")) "#)" )) ")" )); end; :: deftheorem defines :::"latt"::: FILTER_0:def 9 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_filter_0 :::"latt"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "F")) "st" (Bool "(" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "F")))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "F")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) "#)" )) ")" )) ")" )))); registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); cluster (Set ($#k6_filter_0 :::"latt"::: ) "F") -> ($#v3_lattices :::"strict"::: ) ; end; theorem :: FILTER_0:48 (Bool "for" (Set (Var "L")) "being" ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set ($#k1_filter_0 :::"<."::: ) (Set (Var "L")) ($#k1_filter_0 :::".)"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "L")))) ; theorem :: FILTER_0:49 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_filter_0 :::"latt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set "(" ($#k6_filter_0 :::"latt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "F")))) & (Bool (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set "(" ($#k6_filter_0 :::"latt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "F")))) ")" ))) ; theorem :: FILTER_0:50 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_filter_0 :::"latt"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q9")))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p9")) ($#k3_lattices :::""\/""::: ) (Set (Var "q9")))) & (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p9")) ($#k4_lattices :::""/\""::: ) (Set (Var "q9")))) ")" ))))) ; theorem :: FILTER_0:51 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_filter_0 :::"latt"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q9")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "p9")) ($#r3_lattices :::"[="::: ) (Set (Var "q9"))) ")" ))))) ; theorem :: FILTER_0:52 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) )) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set (Var "F"))) "is" ($#v14_lattices :::"upper-bounded"::: ) ))) ; theorem :: FILTER_0:53 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v12_lattices :::"modular"::: ) )) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set (Var "F"))) "is" ($#v12_lattices :::"modular"::: ) ))) ; theorem :: FILTER_0:54 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v11_lattices :::"distributive"::: ) )) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set (Var "F"))) "is" ($#v11_lattices :::"distributive"::: ) ))) ; theorem :: FILTER_0:55 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"I_Lattice":::))) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set (Var "F"))) "is" ($#v3_filter_0 :::"implicative"::: ) ))) ; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k6_filter_0 :::"latt"::: ) (Set ($#k2_filter_0 :::"<."::: ) "p" ($#k2_filter_0 :::".)"::: ) )) -> ($#v13_lattices :::"lower-bounded"::: ) ; end; theorem :: FILTER_0:56 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k6_filter_0 :::"latt"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: FILTER_0:57 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) )) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k6_filter_0 :::"latt"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))))) ; theorem :: FILTER_0:58 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"1_Lattice":::))) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) "is" ($#v15_lattices :::"bounded"::: ) ))) ; theorem :: FILTER_0:59 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"C_Lattice":::)) & (Bool (Set (Var "L")) "is" ($#l3_lattices :::"M_Lattice":::))) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) "is" ($#l3_lattices :::"C_Lattice":::)))) ; theorem :: FILTER_0:60 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"B_Lattice":::))) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) "is" ($#l3_lattices :::"B_Lattice":::)))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "p" :::"<=>"::: "q" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: FILTER_0:def 10 (Set (Set "(" "p" ($#k4_filter_0 :::"=>"::: ) "q" ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" "q" ($#k4_filter_0 :::"=>"::: ) "p" ")" )); end; :: deftheorem defines :::"<=>"::: FILTER_0:def 10 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "q")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "p")) ")" ))))); theorem :: FILTER_0:61 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "p")))))) ; theorem :: FILTER_0:62 (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "FI")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "i")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI"))) & (Bool (Set (Set (Var "j")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))) "holds" (Bool (Set (Set (Var "i")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "FI")))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); func :::"equivalence_wrt"::: "F" -> ($#m1_hidden :::"Relation":::) means :: FILTER_0:def 11 (Bool "(" (Bool (Set ($#k1_relat_1 :::"field"::: ) it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Set (Var "p")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "F") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"equivalence_wrt"::: FILTER_0:def 11 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Set (Var "p")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) ")" ) ")" ) ")" )))); theorem :: FILTER_0:63 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F"))) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: FILTER_0:64 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"I_Lattice":::))) "holds" (Bool (Set ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F"))) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: FILTER_0:65 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F"))) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: FILTER_0:66 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"I_Lattice":::))) "holds" (Bool (Set ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F"))) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: FILTER_0:67 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"I_Lattice":::))) "holds" (Bool (Set ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F"))) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: FILTER_0:68 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#l3_lattices :::"I_Lattice":::))) "holds" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set "(" ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; definitionlet "I" be ($#l3_lattices :::"I_Lattice":::); let "FI" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "I")); :: original: :::"equivalence_wrt"::: redefine func :::"equivalence_wrt"::: "FI" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "I"); end; definitionlet "B" be ($#l3_lattices :::"B_Lattice":::); let "FB" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "B")); :: original: :::"equivalence_wrt"::: redefine func :::"equivalence_wrt"::: "FB" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B"); end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "p" "," "q" :::"are_equivalence_wrt"::: "F" means :: FILTER_0:def 12 (Bool (Set "p" ($#k7_filter_0 :::"<=>"::: ) "q") ($#r2_hidden :::"in"::: ) "F"); end; :: deftheorem defines :::"are_equivalence_wrt"::: FILTER_0:def 12 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "F"))) "iff" (Bool (Set (Set (Var "p")) ($#k7_filter_0 :::"<=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )))); theorem :: FILTER_0:69 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "F"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_filter_0 :::"equivalence_wrt"::: ) (Set (Var "F")))) ")" )))) ; theorem :: FILTER_0:70 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "FB")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "FI")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "i")) "," (Set (Var "i")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FI"))) & (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FB"))) ")" ))))))) ; theorem :: FILTER_0:71 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "q")) "," (Set (Var "p")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "F")))))) ; theorem :: FILTER_0:72 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "FB")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "I")) "being" ($#l3_lattices :::"I_Lattice":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "FI")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FI"))) & (Bool (Set (Var "j")) "," (Set (Var "k")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FI")))) "implies" (Bool (Set (Var "i")) "," (Set (Var "k")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FI"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FB"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FB")))) "implies" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_filter_0 :::"are_equivalence_wrt"::: ) (Set (Var "FB"))) ")" ")" ))))))) ; begin theorem :: FILTER_0:73 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z")) ($#r3_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r3_lattices :::"[="::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "z9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z9")) ($#r3_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "z9")) ($#r3_lattices :::"[="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "z9")) ($#r3_lattices :::"[="::: ) (Set (Var "z"))) ")" )) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_lattices :::""/\""::: ) (Set (Var "y")))))) ; theorem :: FILTER_0:74 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r3_lattices :::"[="::: ) (Set (Var "z"))) & (Bool "(" "for" (Set (Var "z9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "z9"))) & (Bool (Set (Var "y")) ($#r3_lattices :::"[="::: ) (Set (Var "z9")))) "holds" (Bool (Set (Var "z")) ($#r3_lattices :::"[="::: ) (Set (Var "z9"))) ")" )) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_lattices :::""\/""::: ) (Set (Var "y")))))) ;