:: LATTICE6 semantic presentation begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v10_lattices :::"Lattice-like"::: ) -> ($#v4_lattice3 :::"complete"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func "D" :::"%"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) "L" ")" ) equals :: LATTICE6:def 1 "{" (Set "(" (Set (Var "d")) ($#k4_lattice3 :::"%"::: ) ")" ) where d "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) "D") "}" ; end; :: deftheorem defines :::"%"::: LATTICE6:def 1 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "D")) ($#k1_lattice6 :::"%"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "d")) ($#k4_lattice3 :::"%"::: ) ")" ) where d "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" ))); definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Const "L")) ")" ); func :::"%"::: "D" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: LATTICE6:def 2 "{" (Set "(" ($#k5_lattice3 :::"%"::: ) (Set (Var "d")) ")" ) where d "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) "L" ")" ) : (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) "D") "}" ; end; :: deftheorem defines :::"%"::: LATTICE6:def 2 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L")) ")" ) "holds" (Bool (Set ($#k2_lattice6 :::"%"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_lattice3 :::"%"::: ) (Set (Var "d")) ")" ) where d "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L")) ")" ) : (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" ))); registrationlet "L" be ($#v8_struct_0 :::"finite"::: ) ($#l3_lattices :::"Lattice":::); cluster (Set ($#k3_lattice3 :::"LattPOSet"::: ) "L") -> ($#v1_wellfnd1 :::"well_founded"::: ) ; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); attr "L" is :::"noetherian"::: means :: LATTICE6:def 3 (Bool (Set ($#k3_lattice3 :::"LattPOSet"::: ) "L") "is" ($#v1_wellfnd1 :::"well_founded"::: ) ); attr "L" is :::"co-noetherian"::: means :: LATTICE6:def 4 (Bool (Set (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) "L" ")" ) ($#k7_lattice3 :::"~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ); end; :: deftheorem defines :::"noetherian"::: LATTICE6:def 3 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_lattice6 :::"noetherian"::: ) ) "iff" (Bool (Set ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L"))) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) ")" )); :: deftheorem defines :::"co-noetherian"::: LATTICE6:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_lattice6 :::"co-noetherian"::: ) ) "iff" (Bool (Set (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L")) ")" ) ($#k7_lattice3 :::"~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v1_lattice6 :::"noetherian"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v2_lattice6 :::"co-noetherian"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: LATTICE6:1 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_lattice6 :::"noetherian"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k1_lattice2 :::".:"::: ) ) "is" ($#v2_lattice6 :::"co-noetherian"::: ) ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v10_lattices :::"Lattice-like"::: ) -> ($#v1_lattice6 :::"noetherian"::: ) for ($#l3_lattices :::"LattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v10_lattices :::"Lattice-like"::: ) -> ($#v2_lattice6 :::"co-noetherian"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "a" :::"is-upper-neighbour-of"::: "b" means :: LATTICE6:def 5 (Bool "(" (Bool "a" ($#r1_hidden :::"<>"::: ) "b") & (Bool "b" ($#r3_lattices :::"[="::: ) "a") & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "b" ($#r3_lattices :::"[="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r3_lattices :::"[="::: ) "a") & (Bool (Bool "not" (Set (Var "c")) ($#r1_hidden :::"="::: ) "a"))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) "b") ")" ) ")" ); end; :: deftheorem defines :::"is-upper-neighbour-of"::: LATTICE6:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "b"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Bool "not" (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" ) ")" ))); notationlet "L" be ($#l3_lattices :::"Lattice":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym "b" :::"is-lower-neighbour-of"::: "a" for "a" :::"is-upper-neighbour-of"::: "b"; end; theorem :: LATTICE6:2 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "b")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")))) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")))) ")" ")" ))) ; theorem :: LATTICE6:3 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice6 :::"noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "d"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "d")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r3_lattices :::"[="::: ) (Set (Var "d"))) & (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a"))) ")" )))) ; theorem :: LATTICE6:4 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice6 :::"co-noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "d")))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "d")) ($#r3_lattices :::"[="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a"))) ")" )))) ; theorem :: LATTICE6:5 (Bool "for" (Set (Var "L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Bool "not" (Set (Var "b")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))))))) ; theorem :: LATTICE6:6 (Bool "for" (Set (Var "L")) "being" ($#v14_lattices :::"upper-bounded"::: ) ($#v1_lattice6 :::"noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Bool "not" (Set (Var "b")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a"))))) ")" ))) ; theorem :: LATTICE6:7 (Bool "for" (Set (Var "L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Bool "not" (Set (Var "b")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))))))) ; theorem :: LATTICE6:8 (Bool "for" (Set (Var "L")) "being" ($#v13_lattices :::"lower-bounded"::: ) ($#v2_lattice6 :::"co-noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Bool "not" (Set (Var "b")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a"))))) ")" ))) ; definitionlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"*'"::: -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE6:def 6 (Set ($#k16_lattice3 :::""/\""::: ) "(" "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "(" (Bool "a" ($#r3_lattices :::"[="::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) "a") ")" ) "}" "," "L" ")" ); func :::"*'"::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE6:def 7 (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "(" (Bool (Set (Var "d")) ($#r3_lattices :::"[="::: ) "a") & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) "a") ")" ) "}" "," "L" ")" ); end; :: deftheorem defines :::"*'"::: LATTICE6:def 6 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattice6 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ) "}" "," (Set (Var "L")) ")" )))); :: deftheorem defines :::"*'"::: LATTICE6:def 7 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_lattice6 :::"*'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "d")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ) "}" "," (Set (Var "L")) ")" )))); definitionlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); attr "a" is :::"completely-meet-irreducible"::: means :: LATTICE6:def 8 (Bool (Set "a" ($#k3_lattice6 :::"*'"::: ) ) ($#r1_hidden :::"<>"::: ) "a"); attr "a" is :::"completely-join-irreducible"::: means :: LATTICE6:def 9 (Bool (Set ($#k4_lattice6 :::"*'"::: ) "a") ($#r1_hidden :::"<>"::: ) "a"); end; :: deftheorem defines :::"completely-meet-irreducible"::: LATTICE6:def 8 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) ) "iff" (Bool (Set (Set (Var "a")) ($#k3_lattice6 :::"*'"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ))); :: deftheorem defines :::"completely-join-irreducible"::: LATTICE6:def 9 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) ) "iff" (Bool (Set ($#k4_lattice6 :::"*'"::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ))); theorem :: LATTICE6:9 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k3_lattice6 :::"*'"::: ) )) & (Bool (Set ($#k4_lattice6 :::"*'"::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) ")" ))) ; theorem :: LATTICE6:10 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k3_lattice6 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v2_waybel_6 :::"meet-irreducible"::: ) ) ")" )) ; theorem :: LATTICE6:11 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set ($#k4_lattice6 :::"*'"::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v3_waybel_6 :::"join-irreducible"::: ) ) ")" )) ; theorem :: LATTICE6:12 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_lattice6 :::"*'"::: ) ) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_lattice6 :::"*'"::: ) )) ")" ) ")" ))) ; theorem :: LATTICE6:13 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) )) "holds" (Bool "(" (Bool (Set ($#k4_lattice6 :::"*'"::: ) (Set (Var "a"))) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k4_lattice6 :::"*'"::: ) (Set (Var "a")))) ")" ) ")" ))) ; theorem :: LATTICE6:14 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#v1_lattice6 :::"noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) ) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" )) ")" ))) ; theorem :: LATTICE6:15 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#v2_lattice6 :::"co-noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) ) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" )) ")" ))) ; theorem :: LATTICE6:16 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v2_waybel_6 :::"meet-irreducible"::: ) ))) ; theorem :: LATTICE6:17 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#v1_lattice6 :::"noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))))) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) ) "iff" (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v2_waybel_6 :::"meet-irreducible"::: ) ) ")" ))) ; theorem :: LATTICE6:18 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v3_waybel_6 :::"join-irreducible"::: ) ))) ; theorem :: LATTICE6:19 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#v2_lattice6 :::"co-noetherian"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) ) "iff" (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v3_waybel_6 :::"join-irreducible"::: ) ) ")" ))) ; theorem :: LATTICE6:20 (Bool "for" (Set (Var "L")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) )) "implies" (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v2_waybel_6 :::"meet-irreducible"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v2_waybel_6 :::"meet-irreducible"::: ) )) "implies" (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) ) ")" & "(" (Bool (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) )) "implies" (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v3_waybel_6 :::"join-irreducible"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "a")) ($#k4_lattice3 :::"%"::: ) ) "is" ($#v3_waybel_6 :::"join-irreducible"::: ) )) "implies" (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) ) ")" ")" ))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); attr "a" is :::"atomic"::: means :: LATTICE6:def 10 (Bool "a" ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set ($#k5_lattices :::"Bottom"::: ) "L")); attr "a" is :::"co-atomic"::: means :: LATTICE6:def 11 (Bool "a" ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set ($#k6_lattices :::"Top"::: ) "L")); end; :: deftheorem defines :::"atomic"::: LATTICE6:def 10 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v5_lattice6 :::"atomic"::: ) ) "iff" (Bool (Set (Var "a")) ($#r1_lattice6 :::"is-upper-neighbour-of"::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) ")" ))); :: deftheorem defines :::"co-atomic"::: LATTICE6:def 11 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v6_lattice6 :::"co-atomic"::: ) ) "iff" (Bool (Set (Var "a")) ($#r1_lattice6 :::"is-lower-neighbour-of"::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) ")" ))); theorem :: LATTICE6:21 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v5_lattice6 :::"atomic"::: ) )) "holds" (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) ))) ; theorem :: LATTICE6:22 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v6_lattice6 :::"co-atomic"::: ) )) "holds" (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) ))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); attr "L" is :::"atomic"::: means :: LATTICE6:def 12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L" "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v5_lattice6 :::"atomic"::: ) ) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," "L" ")" )) ")" ))); end; :: deftheorem defines :::"atomic"::: LATTICE6:def 12 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v7_lattice6 :::"atomic"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v5_lattice6 :::"atomic"::: ) ) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_lattices :::"strict"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v7_lattice6 :::"atomic"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::); let "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "D" is :::"supremum-dense"::: means :: LATTICE6:def 13 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "ex" (Set (Var "D9")) "being" ($#m1_subset_1 :::"Subset":::) "of" "D" "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "D9")) "," "L" ")" )))); attr "D" is :::"infimum-dense"::: means :: LATTICE6:def 14 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "ex" (Set (Var "D9")) "being" ($#m1_subset_1 :::"Subset":::) "of" "D" "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "D9")) "," "L" ")" )))); end; :: deftheorem defines :::"supremum-dense"::: LATTICE6:def 13 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v8_lattice6 :::"supremum-dense"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "D9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "D9")) "," (Set (Var "L")) ")" )))) ")" ))); :: deftheorem defines :::"infimum-dense"::: LATTICE6:def 14 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v9_lattice6 :::"infimum-dense"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "D9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "D9")) "," (Set (Var "L")) ")" )))) ")" ))); theorem :: LATTICE6:23 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v8_lattice6 :::"supremum-dense"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "d")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) ")" ) "}" "," (Set (Var "L")) ")" ))) ")" ))) ; theorem :: LATTICE6:24 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v9_lattice6 :::"infimum-dense"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" "{" (Set (Var "d")) where d "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "d"))) ")" ) "}" "," (Set (Var "L")) ")" ))) ")" ))) ; theorem :: LATTICE6:25 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v9_lattice6 :::"infimum-dense"::: ) ) "iff" (Bool (Set (Set (Var "D")) ($#k1_lattice6 :::"%"::: ) ) "is" ($#v4_waybel_6 :::"order-generating"::: ) ) ")" ))) ; definitionlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::); func :::"MIRRS"::: "L" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: LATTICE6:def 15 "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) ) "}" ; func :::"JIRRS"::: "L" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: LATTICE6:def 16 "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) ) "}" ; end; :: deftheorem defines :::"MIRRS"::: LATTICE6:def 15 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k5_lattice6 :::"MIRRS"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "a")) "is" ($#v3_lattice6 :::"completely-meet-irreducible"::: ) ) "}" )); :: deftheorem defines :::"JIRRS"::: LATTICE6:def 16 : (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k6_lattice6 :::"JIRRS"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "a")) "is" ($#v4_lattice6 :::"completely-join-irreducible"::: ) ) "}" )); theorem :: LATTICE6:26 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v8_lattice6 :::"supremum-dense"::: ) )) "holds" (Bool (Set ($#k6_lattice6 :::"JIRRS"::: ) (Set (Var "L"))) ($#r1_tarski :::"c="::: ) (Set (Var "D"))))) ; theorem :: LATTICE6:27 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v9_lattice6 :::"infimum-dense"::: ) )) "holds" (Bool (Set ($#k5_lattice6 :::"MIRRS"::: ) (Set (Var "L"))) ($#r1_tarski :::"c="::: ) (Set (Var "D"))))) ; registrationlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#v2_lattice6 :::"co-noetherian"::: ) ($#l3_lattices :::"Lattice":::); cluster (Set ($#k5_lattice6 :::"MIRRS"::: ) "L") -> ($#v9_lattice6 :::"infimum-dense"::: ) ; end; registrationlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#v1_lattice6 :::"noetherian"::: ) ($#l3_lattices :::"Lattice":::); cluster (Set ($#k6_lattice6 :::"JIRRS"::: ) "L") -> ($#v8_lattice6 :::"supremum-dense"::: ) ; end;