:: LATTICE4 semantic presentation begin theorem :: LATTICE4:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y")))) "holds" (Bool "not" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) ")" ) ")" ))) ; begin registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster (Set ($#k1_filter_0 :::"<."::: ) "L" ($#k1_filter_0 :::".)"::: ) ) -> ($#v2_filter_0 :::"prime"::: ) ; end; theorem :: LATTICE4:2 (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 ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "H")) ")" ) ($#k3_filter_0 :::".)"::: ) )) & (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "H")) ")" ) ($#k3_filter_0 :::".)"::: ) )) ")" ))) ; theorem :: LATTICE4:3 (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")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_filter_0 :::"<."::: ) (Set "(" (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "q")) ($#k2_filter_0 :::".)"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "F")) ")" ) ($#k3_filter_0 :::".)"::: ) ))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "q")) ($#k4_lattices :::""/\""::: ) (Set (Var "r"))) ($#r3_lattices :::"[="::: ) (Set (Var "p"))) ")" ))))) ; definitionlet "L1", "L2" be ($#l3_lattices :::"Lattice":::); mode :::"Homomorphism"::: "of" "L1" "," "L2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L2") means :: LATTICE4:def 1 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k3_lattices :::""\/""::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "b1")) ")" ))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k4_lattices :::""/\""::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "b1")) ")" ))) ")" )); end; :: deftheorem defines :::"Homomorphism"::: LATTICE4:def 1 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2"))) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k3_lattices :::""\/""::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "b1")) ")" ))) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k4_lattices :::""/\""::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "b1")) ")" ))) ")" )) ")" ))); theorem :: LATTICE4:4 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a1")) ($#r3_lattices :::"[="::: ) (Set (Var "b1")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a1"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b1"))))))) ; theorem :: LATTICE4:5 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r3_lattices :::"[="::: ) (Set (Var "b1"))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a1"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b1")))) ")" )))) ; theorem :: LATTICE4:6 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) (Bool "ex" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "st" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a1")))))))) ; definitionlet "L1", "L2" be ($#l3_lattices :::"Lattice":::); redefine pred "L1" "," "L2" :::"are_isomorphic"::: means :: LATTICE4:def 2 (Bool "ex" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" "L1" "," "L2" "st" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) )); end; :: deftheorem defines :::"are_isomorphic"::: LATTICE4:def 2 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r1_filter_1 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2")) "st" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) )) ")" )); definitionlet "L1", "L2" be ($#l3_lattices :::"Lattice":::); let "f" be ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Const "L1")) "," (Set (Const "L2")); pred "f" :::"preserves_implication"::: means :: LATTICE4:def 3 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k4_filter_0 :::"=>"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "b1")) ")" )))); pred "f" :::"preserves_top"::: means :: LATTICE4:def 4 (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_lattices :::"Top"::: ) "L1" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) "L2")); pred "f" :::"preserves_bottom"::: means :: LATTICE4:def 5 (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) "L1" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) "L2")); pred "f" :::"preserves_complement"::: means :: LATTICE4:def 6 (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k7_lattices :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k7_lattices :::"`"::: ) ))); end; :: deftheorem defines :::"preserves_implication"::: LATTICE4:def 3 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_lattice4 :::"preserves_implication"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k4_filter_0 :::"=>"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b1")) ")" )))) ")" ))); :: deftheorem defines :::"preserves_top"::: LATTICE4:def 4 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_lattice4 :::"preserves_top"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L2")))) ")" ))); :: deftheorem defines :::"preserves_bottom"::: LATTICE4:def 5 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_lattice4 :::"preserves_bottom"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L2")))) ")" ))); :: deftheorem defines :::"preserves_complement"::: LATTICE4:def 6 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_lattice4 :::"preserves_complement"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a1")) ($#k7_lattices :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a1")) ")" ) ($#k7_lattices :::"`"::: ) ))) ")" ))); definitionlet "L" be ($#l3_lattices :::"Lattice":::); mode ClosedSubset of "L" is ($#v20_lattices :::"meet-closed"::: ) ($#v21_lattices :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "L"; end; theorem :: LATTICE4:7 (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 :::"ClosedSubset":::) "of" (Set (Var "L")))) ; registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v20_lattices :::"meet-closed"::: ) ($#v21_lattices :::"join-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); end; theorem :: LATTICE4:8 (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 (Var "F")) "is" ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "L"))))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "B" be ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); func :::"FinJoin"::: "B" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE4:def 7 (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" "B" "," (Set "(" ($#k3_struct_0 :::"id"::: ) "L" ")" ) ")" ); func :::"FinMeet"::: "B" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE4:def 8 (Set ($#k3_lattice2 :::"FinMeet"::: ) "(" "B" "," (Set "(" ($#k3_struct_0 :::"id"::: ) "L" ")" ) ")" ); end; :: deftheorem defines :::"FinJoin"::: LATTICE4:def 7 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set ($#k1_lattice4 :::"FinJoin"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "L")) ")" ) ")" )))); :: deftheorem defines :::"FinMeet"::: LATTICE4:def 8 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "L")) ")" ) ")" )))); theorem :: LATTICE4:9 (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 ($#k1_lattice4 :::"FinJoin"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "p")) ($#k2_setwiseo :::".}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: LATTICE4:10 (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_lattice4 :::"FinMeet"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "p")) ($#k2_setwiseo :::".}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; begin theorem :: LATTICE4:11 (Bool "for" (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "DL")) "being" ($#v11_lattices :::"distributive"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "DL")) "," (Set (Var "L2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v11_lattices :::"distributive"::: ) )))) ; begin theorem :: LATTICE4:12 (Bool "for" (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "0L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "0L")) "," (Set (Var "L2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "(" (Bool (Set (Var "L2")) "is" ($#v13_lattices :::"lower-bounded"::: ) ) & (Bool (Set (Var "f")) ($#r3_lattice4 :::"preserves_bottom"::: ) ) ")" )))) ; theorem :: LATTICE4:13 (Bool "for" (Set (Var "0L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "0L"))) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "0L")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "0L"))) "holds" (Bool (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "b")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ))))))) ; theorem :: LATTICE4:14 (Bool "for" (Set (Var "0L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "0L"))) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "0L")) "holds" (Bool (Set ($#k1_lattice4 :::"FinJoin"::: ) (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "b")) ($#k2_setwiseo :::".}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_lattice4 :::"FinJoin"::: ) (Set (Var "B")) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))))))) ; theorem :: LATTICE4:15 (Bool "for" (Set (Var "0L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "0L"))) "holds" (Bool (Set (Set "(" ($#k1_lattice4 :::"FinJoin"::: ) (Set (Var "B1")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" ($#k1_lattice4 :::"FinJoin"::: ) (Set (Var "B2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_lattice4 :::"FinJoin"::: ) (Set "(" (Set (Var "B1")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "B2")) ")" ))))) ; theorem :: LATTICE4:16 (Bool "for" (Set (Var "0L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k1_lattice4 :::"FinJoin"::: ) (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "0L"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "0L"))))) ; theorem :: LATTICE4:17 (Bool "for" (Set (Var "0L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "0L")) "st" (Bool (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "0L"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "0L"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_lattice4 :::"FinJoin"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; begin theorem :: LATTICE4:18 (Bool "for" (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "1L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "1L")) "," (Set (Var "L2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "(" (Bool (Set (Var "L2")) "is" ($#v14_lattices :::"upper-bounded"::: ) ) & (Bool (Set (Var "f")) ($#r2_lattice4 :::"preserves_top"::: ) ) ")" )))) ; theorem :: LATTICE4:19 (Bool "for" (Set (Var "1L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k2_lattice4 :::"FinMeet"::: ) (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "1L"))))) ; theorem :: LATTICE4:20 (Bool "for" (Set (Var "1L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "1L")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) "holds" (Bool (Set ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "b")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ))))))) ; theorem :: LATTICE4:21 (Bool "for" (Set (Var "1L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "1L")) "holds" (Bool (Set ($#k2_lattice4 :::"FinMeet"::: ) (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "b")) ($#k2_setwiseo :::".}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B")) ")" ) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))))))) ; theorem :: LATTICE4:22 (Bool "for" (Set (Var "1L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) "holds" (Bool (Set ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))) ; theorem :: LATTICE4:23 (Bool "for" (Set (Var "1L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) "holds" (Bool (Set (Set "(" ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B1")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice4 :::"FinMeet"::: ) (Set "(" (Set (Var "B1")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "B2")) ")" ))))) ; theorem :: LATTICE4:24 (Bool "for" (Set (Var "1L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "1L")) "st" (Bool (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "1L"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "1L"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))))) ; begin theorem :: LATTICE4:25 (Bool "for" (Set (Var "DL")) "being" ($#v11_lattices :::"distributive"::: ) ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "DL"))) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "DL")) "holds" (Bool (Set (Set "(" ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B")) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice4 :::"FinMeet"::: ) (Set "(" (Set "(" (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "DL"))) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "DL")) ")" ) "," (Set (Var "p")) ")" ")" ) ($#k8_setwiseo :::".:"::: ) (Set (Var "B")) ")" )))))) ; begin theorem :: LATTICE4:26 (Bool "for" (Set (Var "CL")) "being" ($#l3_lattices :::"C_Lattice":::) (Bool "for" (Set (Var "IL")) "being" ($#v3_filter_0 :::"implicative"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "IL")) "," (Set (Var "CL")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IL")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "j")) ")" ) ")" )) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")))))))) ; theorem :: LATTICE4:27 (Bool "for" (Set (Var "CL")) "being" ($#l3_lattices :::"C_Lattice":::) (Bool "for" (Set (Var "IL")) "being" ($#v3_filter_0 :::"implicative"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "IL")) "," (Set (Var "CL")) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IL")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" )) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "j")) ")" ))))))) ; theorem :: LATTICE4:28 (Bool "for" (Set (Var "CL")) "being" ($#l3_lattices :::"C_Lattice":::) (Bool "for" (Set (Var "IL")) "being" ($#v3_filter_0 :::"implicative"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "IL")) "," (Set (Var "CL")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) )) "holds" (Bool "(" (Bool (Set (Var "CL")) "is" ($#v3_filter_0 :::"implicative"::: ) ) & (Bool (Set (Var "f")) ($#r1_lattice4 :::"preserves_implication"::: ) ) ")" )))) ; begin theorem :: LATTICE4:29 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "BL")) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "BL"))))) ; theorem :: LATTICE4:30 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "BL")) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "BL"))))) ; theorem :: LATTICE4:31 (Bool "for" (Set (Var "CL")) "being" ($#l3_lattices :::"C_Lattice":::) (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "BL")) "," (Set (Var "CL")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "(" (Bool (Set (Var "CL")) "is" ($#v17_lattices :::"Boolean"::: ) ) & (Bool (Set (Var "f")) ($#r4_lattice4 :::"preserves_complement"::: ) ) ")" )))) ; definitionlet "BL" be ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::); mode :::"Field"::: "of" "BL" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "BL" means :: LATTICE4:def 9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "BL" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ) ($#r2_hidden :::"in"::: ) it) ")" )); end; :: deftheorem defines :::"Field"::: LATTICE4:def 9 : (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "BL")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_lattice4 :::"Field"::: ) "of" (Set (Var "BL"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" )) ")" ))); theorem :: LATTICE4:32 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) (Bool "for" (Set (Var "F")) "being" ($#m2_lattice4 :::"Field"::: ) "of" (Set (Var "BL")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))))) ; theorem :: LATTICE4:33 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) (Bool "for" (Set (Var "F")) "being" ($#m2_lattice4 :::"Field"::: ) "of" (Set (Var "BL")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))))) ; theorem :: LATTICE4:34 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "is" ($#m2_lattice4 :::"Field"::: ) "of" (Set (Var "BL")))) ; theorem :: LATTICE4:35 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m2_lattice4 :::"Field"::: ) "of" (Set (Var "BL")) "holds" (Bool (Set (Var "F")) "is" ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "BL"))))) ; definitionlet "BL" be ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "BL")); func :::"field_by"::: "A" -> ($#m2_lattice4 :::"Field"::: ) "of" "BL" means :: LATTICE4:def 10 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) it) & (Bool "(" "for" (Set (Var "F")) "being" ($#m2_lattice4 :::"Field"::: ) "of" "BL" "st" (Bool (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) ")" ); end; :: deftheorem defines :::"field_by"::: LATTICE4:def 10 : (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "BL")) (Bool "for" (Set (Var "b3")) "being" ($#m2_lattice4 :::"Field"::: ) "of" (Set (Var "BL")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice4 :::"field_by"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "F")) "being" ($#m2_lattice4 :::"Field"::: ) "of" (Set (Var "BL")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) ")" ) ")" )))); definitionlet "BL" be ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "BL")); func :::"SetImp"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "BL" equals :: LATTICE4:def 11 "{" (Set "(" (Set (Var "a")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "b")) ")" ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" "BL" : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "A") ")" ) "}" ; end; :: deftheorem defines :::"SetImp"::: LATTICE4:def 11 : (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "BL")) "holds" (Bool (Set ($#k4_lattice4 :::"SetImp"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "b")) ")" ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) "}" ))); registrationlet "BL" be ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "BL")); cluster (Set ($#k4_lattice4 :::"SetImp"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: LATTICE4:36 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "BL")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_lattice4 :::"SetImp"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "q")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" )))) ; theorem :: LATTICE4:37 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "BL")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k4_lattice4 :::"SetImp"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_lattices :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "q")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" )))) ; definitionlet "BL" be ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::); func :::"comp"::: "BL" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "BL") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "BL") means :: LATTICE4:def 12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "BL" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ))); end; :: deftheorem defines :::"comp"::: LATTICE4:def 12 : (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) ))) ")" ))); theorem :: LATTICE4:38 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "holds" (Bool (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "b")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set "(" ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")) ")" ) ")" ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k7_lattices :::"`"::: ) ")" )))))) ; theorem :: LATTICE4:39 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "holds" (Bool (Set (Set "(" ($#k1_lattice4 :::"FinJoin"::: ) (Set (Var "B")) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")) ")" ) ")" )))) ; theorem :: LATTICE4:40 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "BL")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "holds" (Bool (Set ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "b")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set "(" ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_lattice2 :::"FinMeet"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")) ")" ) ")" ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k7_lattices :::"`"::: ) ")" )))))) ; theorem :: LATTICE4:41 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "holds" (Bool (Set (Set "(" ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B")) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")) ")" ) ")" )))) ; theorem :: LATTICE4:42 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "AF")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "BL")) "st" (Bool (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "BL"))) ($#r2_hidden :::"in"::: ) (Set (Var "AF"))) & (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "BL"))) ($#r2_hidden :::"in"::: ) (Set (Var "AF")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k4_lattice4 :::"SetImp"::: ) (Set (Var "AF"))))) "holds" (Bool "ex" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) "st" (Bool "(" (Bool (Set (Var "B0")) ($#r1_tarski :::"c="::: ) (Set ($#k4_lattice4 :::"SetImp"::: ) (Set (Var "AF")))) & (Bool (Set ($#k2_lattice2 :::"FinJoin"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k5_lattice4 :::"comp"::: ) (Set (Var "BL")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B0")))) ")" ))))) ; theorem :: LATTICE4:43 (Bool "for" (Set (Var "BL")) "being" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "AF")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"ClosedSubset":::) "of" (Set (Var "BL")) "st" (Bool (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "BL"))) ($#r2_hidden :::"in"::: ) (Set (Var "AF"))) & (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "BL"))) ($#r2_hidden :::"in"::: ) (Set (Var "AF")))) "holds" (Bool "{" (Set "(" ($#k2_lattice4 :::"FinMeet"::: ) (Set (Var "B")) ")" ) where B "is" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "BL"))) : (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k4_lattice4 :::"SetImp"::: ) (Set (Var "AF")))) "}" ($#r1_hidden :::"="::: ) (Set ($#k3_lattice4 :::"field_by"::: ) (Set (Var "AF")))))) ;