:: FILTER_2 semantic presentation begin theorem :: FILTER_2:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_realset1 :::"||"::: ) (Set (Var "S"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v1_binop_1 :::"commutative"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v2_binop_1 :::"associative"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) ")" ")" ))))) ; theorem :: FILTER_2:2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_realset1 :::"||"::: ) (Set (Var "S")))) & (Bool (Set (Var "d9")) ($#r1_hidden :::"="::: ) (Set (Var "d")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "d")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "f")))) "implies" (Bool (Set (Var "d9")) ($#r1_binop_1 :::"is_a_left_unity_wrt"::: ) (Set (Var "g"))) ")" & "(" (Bool (Bool (Set (Var "d")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "f")))) "implies" (Bool (Set (Var "d9")) ($#r2_binop_1 :::"is_a_right_unity_wrt"::: ) (Set (Var "g"))) ")" & "(" (Bool (Bool (Set (Var "d")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "f")))) "implies" (Bool (Set (Var "d9")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "g"))) ")" ")" ))))))) ; theorem :: FILTER_2:3 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_realset1 :::"||"::: ) (Set (Var "S")))) & (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_realset1 :::"||"::: ) (Set (Var "S"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f1")) ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) (Set (Var "f2")))) "implies" (Bool (Set (Var "g1")) ($#r4_binop_1 :::"is_left_distributive_wrt"::: ) (Set (Var "g2"))) ")" & "(" (Bool (Bool (Set (Var "f1")) ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) (Set (Var "f2")))) "implies" (Bool (Set (Var "g1")) ($#r5_binop_1 :::"is_right_distributive_wrt"::: ) (Set (Var "g2"))) ")" ")" ))))) ; theorem :: FILTER_2:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_realset1 :::"||"::: ) (Set (Var "S")))) & (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_realset1 :::"||"::: ) (Set (Var "S")))) & (Bool (Set (Var "f1")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "f2")))) "holds" (Bool (Set (Var "g1")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "g2"))))))) ; theorem :: FILTER_2:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_realset1 :::"||"::: ) (Set (Var "S")))) & (Bool (Set (Var "g2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_realset1 :::"||"::: ) (Set (Var "S")))) & (Bool (Set (Var "f1")) ($#r1_lattice2 :::"absorbs"::: ) (Set (Var "f2")))) "holds" (Bool (Set (Var "g1")) ($#r1_lattice2 :::"absorbs"::: ) (Set (Var "g2"))))))) ; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X1", "X2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); :: original: :::"="::: redefine pred "X1" :::"="::: "X2" means :: FILTER_2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X1") "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X2") ")" )); end; :: deftheorem defines :::"="::: FILTER_2:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_filter_2 :::"="::: ) (Set (Var "X2"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) ")" )) ")" ))); theorem :: FILTER_2:6 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool (Set (Set (Var "L1")) ($#k1_lattice2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L2")) ($#k1_lattice2 :::".:"::: ) ))) ; theorem :: FILTER_2:7 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) ($#k1_lattice2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" ))) ; theorem :: FILTER_2:8 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k1_lattices :::""\/""::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k1_lattices :::""\/""::: ) (Set (Var "b2")))) & (Bool (Set (Set (Var "a1")) ($#k2_lattices :::""/\""::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k2_lattices :::""/\""::: ) (Set (Var "b2")))) & "(" (Bool (Bool (Set (Var "a1")) ($#r1_lattices :::"[="::: ) (Set (Var "b1")))) "implies" (Bool (Set (Var "a2")) ($#r1_lattices :::"[="::: ) (Set (Var "b2"))) ")" & "(" (Bool (Bool (Set (Var "a2")) ($#r1_lattices :::"[="::: ) (Set (Var "b2")))) "implies" (Bool (Set (Var "a1")) ($#r1_lattices :::"[="::: ) (Set (Var "b1"))) ")" ")" )))) ; theorem :: FILTER_2:9 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"0_Lattice":::) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L2"))))) ; theorem :: FILTER_2:10 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"1_Lattice":::) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L2"))))) ; theorem :: FILTER_2:11 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"C_Lattice":::) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "a1")) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Var "a2")) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "b2")))))) ; theorem :: FILTER_2:12 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"B_Lattice":::) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k7_lattices :::"`"::: ) ))))) ; theorem :: FILTER_2:13 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (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 "X"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L"))))) ; theorem :: FILTER_2:14 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (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 "X"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L"))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); mode Ideal of "L" is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v18_lattices :::"initial"::: ) ($#v21_lattices :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "L"; end; theorem :: FILTER_2:15 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L1")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L2"))))) ; theorem :: FILTER_2:16 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L1")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L2"))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "p" :::".:"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" "L" ($#k1_lattice2 :::".:"::: ) ")" ) equals :: FILTER_2:def 2 "p"; end; :: deftheorem defines :::".:"::: FILTER_2: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 (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p"))))); definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Const "L")) ($#k1_lattice2 :::".:"::: ) ")" ); func :::".:"::: "p" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: FILTER_2:def 3 "p"; end; :: deftheorem defines :::".:"::: FILTER_2:def 3 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool (Set ($#k2_filter_2 :::".:"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))); theorem :: FILTER_2:17 (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 "p9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool "(" (Bool (Set ($#k2_filter_2 :::".:"::: ) (Set "(" (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "(" ($#k2_filter_2 :::".:"::: ) (Set (Var "p9")) ")" ) ($#k1_filter_2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) ")" )))) ; theorem :: FILTER_2:18 (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 "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k1_filter_2 :::".:"::: ) ")" ))) & (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "q")) ($#k1_filter_2 :::".:"::: ) ")" ))) & (Bool (Set (Set (Var "p9")) ($#k4_lattices :::""/\""::: ) (Set (Var "q9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_filter_2 :::".:"::: ) (Set (Var "p9")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" ($#k2_filter_2 :::".:"::: ) (Set (Var "q9")) ")" ))) & (Bool (Set (Set (Var "p9")) ($#k3_lattices :::""\/""::: ) (Set (Var "q9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_filter_2 :::".:"::: ) (Set (Var "p9")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" ($#k2_filter_2 :::".:"::: ) (Set (Var "q9")) ")" ))) ")" )))) ; theorem :: FILTER_2:19 (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 "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "implies" (Bool (Set (Set (Var "q")) ($#k1_filter_2 :::".:"::: ) ) ($#r3_lattices :::"[="::: ) (Set (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_filter_2 :::".:"::: ) ) ($#r3_lattices :::"[="::: ) (Set (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) ))) "implies" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) ")" & "(" (Bool (Bool (Set (Var "p9")) ($#r3_lattices :::"[="::: ) (Set (Var "q9")))) "implies" (Bool (Set ($#k2_filter_2 :::".:"::: ) (Set (Var "q9"))) ($#r3_lattices :::"[="::: ) (Set ($#k2_filter_2 :::".:"::: ) (Set (Var "p9")))) ")" & "(" (Bool (Bool (Set ($#k2_filter_2 :::".:"::: ) (Set (Var "q9"))) ($#r3_lattices :::"[="::: ) (Set ($#k2_filter_2 :::".:"::: ) (Set (Var "p9"))))) "implies" (Bool (Set (Var "p9")) ($#r3_lattices :::"[="::: ) (Set (Var "q9"))) ")" ")" )))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func "X" :::".:"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "L" ($#k1_lattice2 :::".:"::: ) ")" ) equals :: FILTER_2:def 4 "X"; end; :: deftheorem defines :::".:"::: FILTER_2:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "X")) ($#k3_filter_2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "X"))))); definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "L")) ($#k1_lattice2 :::".:"::: ) ")" ); func :::".:"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: FILTER_2:def 5 "X"; end; :: deftheorem defines :::".:"::: FILTER_2:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool (Set ($#k4_filter_2 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))); registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D" ($#k3_filter_2 :::".:"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "L")) ($#k1_lattice2 :::".:"::: ) ")" ); cluster (Set ($#k4_filter_2 :::".:"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "S" be ($#v20_lattices :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "S" ($#k3_filter_2 :::".:"::: ) ) -> ($#v21_lattices :::"join-closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "L" ($#k1_lattice2 :::".:"::: ) ")" ); end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "S" be ($#v21_lattices :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "S" ($#k3_filter_2 :::".:"::: ) ) -> ($#v20_lattices :::"meet-closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "L" ($#k1_lattice2 :::".:"::: ) ")" ); end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "S" be ($#v20_lattices :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "L")) ($#k1_lattice2 :::".:"::: ) ")" ); cluster (Set ($#k4_filter_2 :::".:"::: ) "S") -> ($#v21_lattices :::"join-closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "L"; end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "S" be ($#v21_lattices :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "L")) ($#k1_lattice2 :::".:"::: ) ")" ); cluster (Set ($#k4_filter_2 :::".:"::: ) "S") -> ($#v20_lattices :::"meet-closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "L"; end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#v19_lattices :::"final"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "F" ($#k3_filter_2 :::".:"::: ) ) -> ($#v18_lattices :::"initial"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "L" ($#k1_lattice2 :::".:"::: ) ")" ); end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#v18_lattices :::"initial"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "F" ($#k3_filter_2 :::".:"::: ) ) -> ($#v19_lattices :::"final"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "L" ($#k1_lattice2 :::".:"::: ) ")" ); end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#v19_lattices :::"final"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "L")) ($#k1_lattice2 :::".:"::: ) ")" ); cluster (Set ($#k4_filter_2 :::".:"::: ) "F") -> ($#v18_lattices :::"initial"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "L"; end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "F" be ($#v18_lattices :::"initial"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "L")) ($#k1_lattice2 :::".:"::: ) ")" ); cluster (Set "F" ($#k3_filter_2 :::".:"::: ) ) -> ($#v19_lattices :::"final"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "L"; end; theorem :: FILTER_2:20 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" )) ")" ))) ; theorem :: FILTER_2:21 (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 :::"Ideal":::) "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")) ($#k3_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 "q")) ($#r3_lattices :::"[="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) ")" ) ")" ))) ; theorem :: FILTER_2:22 (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 "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "q")) ($#k4_lattices :::""/\""::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )))) ; theorem :: FILTER_2:23 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))))) ; theorem :: FILTER_2:24 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))))) ; theorem :: FILTER_2:25 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")))) ; theorem :: FILTER_2:26 (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 :::"Ideal":::) "of" (Set (Var "L")))) "holds" (Bool (Set (Var "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) ))) ; begin theorem :: FILTER_2:27 (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 :::"Ideal":::) "of" (Set (Var "L")))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); func :::"(.":::"L":::".>"::: -> ($#m1_subset_1 :::"Ideal":::) "of" "L" equals :: FILTER_2:def 6 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"); end; :: deftheorem defines :::"(."::: FILTER_2:def 6 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k5_filter_2 :::"(."::: ) (Set (Var "L")) ($#k5_filter_2 :::".>"::: ) ) ($#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 :::"Ideal":::) "of" "L" equals :: FILTER_2:def 7 "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "q")) ($#r3_lattices :::"[="::: ) "p") "}" ; end; :: deftheorem defines :::"(."::: FILTER_2:def 7 : (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 ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "q")) ($#r3_lattices :::"[="::: ) (Set (Var "p"))) "}" ))); theorem :: FILTER_2:28 (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 ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) )) "iff" (Bool (Set (Var "q")) ($#r3_lattices :::"[="::: ) (Set (Var "p"))) ")" ))) ; theorem :: FILTER_2:29 (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 "(" (Bool (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set "(" (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) ")" ) ($#k2_filter_0 :::".)"::: ) )) & (Bool (Set ($#k6_filter_2 :::"(."::: ) (Set "(" (Set (Var "p")) ($#k1_filter_2 :::".:"::: ) ")" ) ($#k6_filter_2 :::".>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )) ")" ))) ; theorem :: FILTER_2:30 (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 ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) )) & (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) )) & (Bool (Set (Set (Var "q")) ($#k4_lattices :::""/\""::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) )) ")" ))) ; theorem :: FILTER_2:31 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) )) "holds" (Bool (Set ($#k5_filter_2 :::"(."::: ) (Set (Var "L")) ($#k5_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k6_filter_2 :::"(."::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_filter_2 :::".>"::: ) ))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "L")); pred "I" :::"is_max-ideal"::: means :: FILTER_2:def 8 (Bool "(" (Bool "I" ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool "(" "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" "L" "st" (Bool (Bool "I" ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))) "holds" (Bool "I" ($#r1_filter_2 :::"="::: ) (Set (Var "J"))) ")" ) ")" ); end; :: deftheorem defines :::"is_max-ideal"::: FILTER_2:def 8 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r2_filter_2 :::"is_max-ideal"::: ) ) "iff" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool "(" "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) "holds" (Bool (Set (Var "I")) ($#r1_filter_2 :::"="::: ) (Set (Var "J"))) ")" ) ")" ) ")" ))); theorem :: FILTER_2:32 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r2_filter_2 :::"is_max-ideal"::: ) ) "iff" (Bool (Set (Set (Var "I")) ($#k3_filter_2 :::".:"::: ) ) "is" ($#v1_filter_0 :::"being_ultrafilter"::: ) ) ")" ))) ; theorem :: FILTER_2:33 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) )) "holds" (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r2_filter_2 :::"is_max-ideal"::: ) ) ")" )))) ; theorem :: FILTER_2:34 (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")) ($#k3_lattices :::""\/""::: ) (Set (Var "r"))) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: FILTER_2:35 (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"::: ) ) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "I")) ($#r2_filter_2 :::"is_max-ideal"::: ) ) ")" )))) ; 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 :::"Ideal":::) "of" "L" means :: FILTER_2:def 9 (Bool "(" (Bool "D" ($#r1_tarski :::"c="::: ) it) & (Bool "(" "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" "L" "st" (Bool (Bool "D" ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "I"))) ")" ) ")" ); end; :: deftheorem defines :::"(."::: FILTER_2:def 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")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) )) "iff" (Bool "(" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "I"))) ")" ) ")" ) ")" )))); theorem :: FILTER_2:36 (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 "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool "(" (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "D")) ($#k3_filter_2 :::".:"::: ) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) )) & (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D")) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "D")) ($#k3_filter_2 :::".:"::: ) ")" ) ($#k7_filter_2 :::".>"::: ) )) & (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set "(" ($#k4_filter_2 :::".:"::: ) (Set (Var "D9")) ")" ) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D9")) ($#k7_filter_2 :::".>"::: ) )) & (Bool (Set ($#k3_filter_0 :::"<."::: ) (Set (Var "D9")) ($#k3_filter_0 :::".)"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set "(" ($#k4_filter_2 :::".:"::: ) (Set (Var "D9")) ")" ) ($#k7_filter_2 :::".>"::: ) )) ")" )))) ; theorem :: FILTER_2:37 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "I")) ($#k7_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set (Var "I"))))) ; theorem :: FILTER_2:38 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "," (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 (Bool (Set (Var "D1")) ($#r1_tarski :::"c="::: ) (Set (Var "D2")))) "implies" (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D1")) ($#k7_filter_2 :::".>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D2")) ($#k7_filter_2 :::".>"::: ) )) ")" & (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) ) ($#k7_filter_2 :::".>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) )) ")" ))) ; theorem :: FILTER_2:39 (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 ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) ))))) ; theorem :: FILTER_2:40 (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_filter_2 :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ))))) ; theorem :: FILTER_2:41 (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" ($#v14_lattices :::"upper-bounded"::: ) ) & (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k5_filter_2 :::"(."::: ) (Set (Var "L")) ($#k5_filter_2 :::".>"::: ) )) & (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D")) ($#k7_filter_2 :::".>"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) ")" ))) ; theorem :: FILTER_2:42 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) ) & (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_filter_2 :::"="::: ) (Set ($#k5_filter_2 :::"(."::: ) (Set (Var "L")) ($#k5_filter_2 :::".>"::: ) )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) ")" ))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "L")); attr "I" is :::"prime"::: means :: FILTER_2:def 10 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "I") "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "I") "or" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "I") ")" ) ")" )); end; :: deftheorem defines :::"prime"::: FILTER_2:def 10 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_filter_2 :::"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")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) "or" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" ) ")" )) ")" ))); theorem :: FILTER_2:43 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_filter_2 :::"prime"::: ) ) "iff" (Bool (Set (Set (Var "I")) ($#k3_filter_2 :::".:"::: ) ) "is" ($#v2_filter_0 :::"prime"::: ) ) ")" ))) ; 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_2:def 11 "{" (Set "(" (Set (Var "p")) ($#k3_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_2:def 11 : (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")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "p")) ($#k3_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" ($#k8_filter_2 :::""\/""::: ) "D2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: FILTER_2:44 (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")) (Bool "for" (Set (Var "D19")) "," (Set (Var "D29")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "D1")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "D1")) ($#k3_filter_2 :::".:"::: ) ")" ) ($#k5_filter_0 :::""/\""::: ) (Set "(" (Set (Var "D2")) ($#k3_filter_2 :::".:"::: ) ")" ))) & (Bool (Set (Set "(" (Set (Var "D1")) ($#k3_filter_2 :::".:"::: ) ")" ) ($#k8_filter_2 :::""\/""::: ) (Set "(" (Set (Var "D2")) ($#k3_filter_2 :::".:"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "D1")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D2")))) & (Bool (Set (Set (Var "D19")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "D29"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_filter_2 :::".:"::: ) (Set (Var "D19")) ")" ) ($#k5_filter_0 :::""/\""::: ) (Set "(" ($#k4_filter_2 :::".:"::: ) (Set (Var "D29")) ")" ))) & (Bool (Set (Set "(" ($#k4_filter_2 :::".:"::: ) (Set (Var "D19")) ")" ) ($#k8_filter_2 :::""\/""::: ) (Set "(" ($#k4_filter_2 :::".:"::: ) (Set (Var "D29")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "D19")) ($#k5_filter_0 :::""/\""::: ) (Set (Var "D29")))) ")" )))) ; theorem :: FILTER_2:45 (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")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D1")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "D2")))) & (Bool (Set (Set (Var "q")) ($#k3_lattices :::""\/""::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D1")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "D2")))) ")" )))) ; theorem :: FILTER_2:46 (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")) ($#k8_filter_2 :::""\/""::: ) (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")) ($#k3_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_2:47 (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")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "D2"))) ($#r1_filter_2 :::"="::: ) (Set (Set (Var "D2")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "D1")))))) ; registrationlet "L" be ($#l3_lattices :::"D_Lattice":::); let "I1", "I2" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "L")); cluster (Set "I1" ($#k8_filter_2 :::""\/""::: ) "I2") -> ($#v18_lattices :::"initial"::: ) ($#v21_lattices :::"join-closed"::: ) ; end; theorem :: FILTER_2:48 (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 ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "D1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "D2")) ")" ) ($#k7_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D1")) ($#k7_filter_2 :::".>"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "D2")) ")" ) ($#k7_filter_2 :::".>"::: ) )) & (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "D1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "D2")) ")" ) ($#k7_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "D1")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set (Var "D2")) ($#k7_filter_2 :::".>"::: ) ) ")" ) ($#k7_filter_2 :::".>"::: ) )) ")" ))) ; theorem :: FILTER_2:49 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "I")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "J")) ")" ) ($#k7_filter_2 :::".>"::: ) ) ($#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 (Var "r")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "J"))) ")" )) "}" ))) ; theorem :: FILTER_2:50 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "I")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "J")))) & (Bool (Set (Var "J")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "I")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "J")))) ")" ))) ; theorem :: FILTER_2:51 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "I")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "J")) ")" ) ($#k7_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "I")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "J")) ")" ) ($#k7_filter_2 :::".>"::: ) )))) ; theorem :: FILTER_2:52 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#l3_lattices :::"C_Lattice":::)) "iff" (Bool (Set (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ) "is" ($#l3_lattices :::"C_Lattice":::)) ")" )) ; theorem :: FILTER_2:53 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#l3_lattices :::"B_Lattice":::)) "iff" (Bool (Set (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ) "is" ($#l3_lattices :::"B_Lattice":::)) ")" )) ; registrationlet "B" be ($#l3_lattices :::"B_Lattice":::); cluster (Set "B" ($#k1_lattice2 :::".:"::: ) ) -> ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ; end; theorem :: FILTER_2:54 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "B")) ($#k1_lattice2 :::".:"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_filter_2 :::".:"::: ) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) )) & (Bool (Set (Set "(" ($#k2_filter_2 :::".:"::: ) (Set (Var "a9")) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k7_lattices :::"`"::: ) )) ")" )))) ; theorem :: FILTER_2:55 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "IB")) "," (Set (Var "JB")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "B")) "holds" (Bool (Set ($#k7_filter_2 :::"(."::: ) (Set "(" (Set (Var "IB")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "JB")) ")" ) ($#k7_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set (Set (Var "IB")) ($#k8_filter_2 :::""\/""::: ) (Set (Var "JB")))))) ; theorem :: FILTER_2:56 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "IB")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "IB")) ($#r2_filter_2 :::"is_max-ideal"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IB")) ($#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 "IB"))) "or" (Bool (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IB"))) ")" ) ")" ) ")" ) ")" ))) ; theorem :: FILTER_2:57 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "IB")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "IB")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_filter_2 :::"(."::: ) (Set (Var "B")) ($#k5_filter_2 :::".>"::: ) )) & (Bool (Set (Var "IB")) "is" ($#v1_filter_2 :::"prime"::: ) ) ")" ) "iff" (Bool (Set (Var "IB")) ($#r2_filter_2 :::"is_max-ideal"::: ) ) ")" ))) ; theorem :: FILTER_2:58 (Bool "for" (Set (Var "B")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "IB")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "IB")) ($#r2_filter_2 :::"is_max-ideal"::: ) )) "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 "IB"))) "iff" (Bool (Bool "not" (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IB")))) ")" )))) ; theorem :: FILTER_2:59 (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 "IB")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "IB")) ($#r2_filter_2 :::"is_max-ideal"::: ) ) & (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "IB"))) & (Bool (Bool "not" (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "IB")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "IB")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "IB"))) ")" ) ")" ) ")" )))) ; theorem :: FILTER_2:60 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P"))) "is" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "P"))) & (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P"))) "is" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "P"))) ")" ))) ; theorem :: FILTER_2:61 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P"))))) "holds" (Bool "(" (Bool (Set (Var "o1")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "o1")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "o2")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "o2")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "o1")) ($#r1_lattice2 :::"absorbs"::: ) (Set (Var "o2"))) & (Bool (Set (Var "o2")) ($#r1_lattice2 :::"absorbs"::: ) (Set (Var "o1"))) ")" )))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); assume (Bool (Set (Const "p")) ($#r3_lattices :::"[="::: ) (Set (Const "q"))) ; func :::"[#":::"p" "," "q":::"#]"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" "L" equals :: FILTER_2:def 12 "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "(" (Bool "p" ($#r3_lattices :::"[="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r3_lattices :::"[="::: ) "q") ")" ) "}" ; end; :: deftheorem defines :::"[#"::: FILTER_2:def 12 : (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 "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) ")" ) "}" ))); theorem :: FILTER_2:62 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (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 "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) )) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) ")" ) ")" ))) ; theorem :: FILTER_2:63 (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 "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) )) ")" ))) ; theorem :: FILTER_2:64 (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 ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k9_filter_2 :::"#]"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: FILTER_2:65 (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 ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k9_filter_2 :::"#]"::: ) )))) ; theorem :: FILTER_2:66 (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" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ($#r1_filter_2 :::"="::: ) (Set ($#k9_filter_2 :::"[#"::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" ) "," (Set (Var "p")) ($#k9_filter_2 :::"#]"::: ) )))) ; theorem :: FILTER_2:67 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Var "F2")))) "holds" (Bool (Set ($#k6_filter_0 :::"latt"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_filter_0 :::"latt"::: ) (Set (Var "F2"))))))) ; begin notationlet "L" be ($#l3_lattices :::"Lattice":::); synonym :::"Sublattice"::: "of" "L" for :::"SubLattice"::: "of" "L"; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); redefine mode :::"SubLattice"::: "of" "L" means :: FILTER_2:def 13 (Bool "ex" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" "L"(Bool "ex" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set (Var "P")) "," (Set (Var "o1")) "," (Set (Var "o2")) "#)" )) ")" ))); end; :: deftheorem defines :::"Sublattice"::: FILTER_2:def 13 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b2")) "being" ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_nat_lat :::"Sublattice"::: ) "of" (Set (Var "L"))) "iff" (Bool "ex" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L"))(Bool "ex" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set (Var "P")) "," (Set (Var "o1")) "," (Set (Var "o2")) "#)" )) ")" ))) ")" ))); theorem :: FILTER_2:68 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "K")) "being" ($#m2_nat_lat :::"Sublattice"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Const "L")); func :::"latt"::: "(" "L" "," "P" ")" -> ($#m2_nat_lat :::"Sublattice"::: ) "of" "L" means :: FILTER_2:def 14 (Bool "ex" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" "P" "st" (Bool "(" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) "P")) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) "P")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" "P" "," (Set (Var "o1")) "," (Set (Var "o2")) "#)" )) ")" )); end; :: deftheorem defines :::"latt"::: FILTER_2:def 14 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m2_nat_lat :::"Sublattice"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" )) "iff" (Bool "ex" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set (Var "P")) "," (Set (Var "o1")) "," (Set (Var "o2")) "#)" )) ")" )) ")" )))); registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Const "L")); cluster (Set ($#k10_filter_2 :::"latt"::: ) "(" "L" "," "P" ")" ) -> ($#v3_lattices :::"strict"::: ) ; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "l" be ($#m2_nat_lat :::"Sublattice"::: ) "of" (Set (Const "L")); :: original: :::".:"::: redefine func "l" :::".:"::: -> ($#v3_lattices :::"strict"::: ) ($#m2_nat_lat :::"Sublattice"::: ) "of" (Set "L" ($#k1_lattice2 :::".:"::: ) ); end; theorem :: FILTER_2:69 (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 ($#k6_filter_0 :::"latt"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "F")) ")" )))) ; theorem :: FILTER_2:70 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set "(" (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ")" ) "," (Set "(" (Set (Var "P")) ($#k3_filter_2 :::".:"::: ) ")" ) ")" ")" ) ($#k11_filter_2 :::".:"::: ) )))) ; theorem :: FILTER_2:71 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k5_filter_2 :::"(."::: ) (Set (Var "L")) ($#k5_filter_2 :::".>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k1_filter_0 :::"<."::: ) (Set (Var "L")) ($#k1_filter_0 :::".)"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) ")" )) ; theorem :: FILTER_2:72 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) & (Bool (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set (Var "P")))) ")" ))) ; theorem :: FILTER_2:73 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ")" ) "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_2:74 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ")" ) "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_2:75 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "I")) ")" ) "is" ($#v13_lattices :::"lower-bounded"::: ) ))) ; theorem :: FILTER_2:76 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v12_lattices :::"modular"::: ) )) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ) "is" ($#v12_lattices :::"modular"::: ) ))) ; theorem :: FILTER_2:77 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v11_lattices :::"distributive"::: ) )) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set (Var "P")) ")" ) "is" ($#v11_lattices :::"distributive"::: ) ))) ; theorem :: FILTER_2:78 (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" ($#v3_filter_0 :::"implicative"::: ) ) & (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) ) ")" ) "is" ($#v3_filter_0 :::"implicative"::: ) ))) ; registrationlet "L" be ($#l3_lattices :::"Lattice":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k10_filter_2 :::"latt"::: ) "(" "L" "," (Set ($#k6_filter_2 :::"(."::: ) "p" ($#k6_filter_2 :::".>"::: ) ) ")" ) -> ($#v14_lattices :::"upper-bounded"::: ) ; end; theorem :: FILTER_2:79 (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 ($#k6_lattices :::"Top"::: ) (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: FILTER_2:80 (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" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool "(" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ")" ) "is" ($#v13_lattices :::"lower-bounded"::: ) ) & (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) ")" ))) ; theorem :: FILTER_2:81 (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" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ")" ) "is" ($#v15_lattices :::"bounded"::: ) ))) ; theorem :: FILTER_2:82 (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 "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) ) ")" ) "is" ($#v15_lattices :::"bounded"::: ) ) & (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" ))) ; theorem :: FILTER_2:83 (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" ($#v12_lattices :::"modular"::: ) )) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k6_filter_2 :::"(."::: ) (Set (Var "p")) ($#k6_filter_2 :::".>"::: ) ) ")" ) "is" ($#l3_lattices :::"C_Lattice":::)))) ; theorem :: FILTER_2:84 (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 :::"C_Lattice":::)) & (Bool (Set (Var "L")) "is" ($#v12_lattices :::"modular"::: ) ) & (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) ) ")" ) "is" ($#l3_lattices :::"C_Lattice":::)))) ; theorem :: FILTER_2:85 (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 :::"B_Lattice":::)) & (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k10_filter_2 :::"latt"::: ) "(" (Set (Var "L")) "," (Set ($#k9_filter_2 :::"[#"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k9_filter_2 :::"#]"::: ) ) ")" ) "is" ($#l3_lattices :::"B_Lattice":::)))) ; theorem :: FILTER_2:86 (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 :::"Ideal":::) "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")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )) ")" ))) ;