:: WAYBEL_8 semantic presentation begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"CompactSublatt"::: "L" -> ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L" means :: WAYBEL_8:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "iff" (Bool (Set (Var "x")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" )); end; :: deftheorem defines :::"CompactSublatt"::: WAYBEL_8:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) "iff" (Bool (Set (Var "x")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" )) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ; end; theorem :: WAYBEL_8:1 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )))) "holds" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))))) ; theorem :: WAYBEL_8:2 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) "is" ($#v1_waybel_6 :::"Open"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))) "iff" (Bool (Set (Var "x")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ))) ; theorem :: WAYBEL_8:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L"))) "is" ($#v6_yellow_0 :::"join-inheriting"::: ) ) & (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ))) ")" )) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"compactbelow"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: WAYBEL_8:def 2 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "(" (Bool "x" ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ) "}" ; end; :: deftheorem defines :::"compactbelow"::: WAYBEL_8:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ) "}" ))); theorem :: WAYBEL_8:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL_8:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )))))) ; theorem :: WAYBEL_8:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k2_waybel_8 :::"compactbelow"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"satisfying_axiom_K"::: means :: WAYBEL_8:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"satisfying_axiom_K"::: WAYBEL_8:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_waybel_8 :::"satisfying_axiom_K"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x")) ")" )))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"algebraic"::: means :: WAYBEL_8:def 4 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Bool "not" (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" ) ")" ) & (Bool "L" "is" ($#v24_waybel_0 :::"up-complete"::: ) ) & (Bool "L" "is" ($#v1_waybel_8 :::"satisfying_axiom_K"::: ) ) ")" ); end; :: deftheorem defines :::"algebraic"::: WAYBEL_8:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" ) ")" ) & (Bool (Set (Var "L")) "is" ($#v24_waybel_0 :::"up-complete"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_waybel_8 :::"satisfying_axiom_K"::: ) ) ")" ) ")" )); theorem :: WAYBEL_8:7 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ))) & (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) ")" )) ")" ) ")" ) ")" )) ; registration cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v2_waybel_8 :::"algebraic"::: ) -> ($#v3_waybel_3 :::"continuous"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v2_waybel_8 :::"algebraic"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v1_waybel_8 :::"satisfying_axiom_K"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) "L") -> ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"arithmetic"::: means :: WAYBEL_8:def 5 (Bool "(" (Bool "L" "is" ($#v2_waybel_8 :::"algebraic"::: ) ) & (Bool (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) "L") "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) ")" ); end; :: deftheorem defines :::"arithmetic"::: WAYBEL_8:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_8 :::"arithmetic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) & (Bool (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) ")" ) ")" )); begin registration cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_waybel_8 :::"arithmetic"::: ) -> ($#v2_waybel_8 :::"algebraic"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#v7_struct_0 :::"trivial"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) -> ($#v3_waybel_8 :::"arithmetic"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: WAYBEL_8:8 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v24_waybel_0 :::"up-complete"::: ) )) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "x1")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y1")))) "holds" (Bool (Set (Var "x2")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y2")))))) ; theorem :: WAYBEL_8:9 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v24_waybel_0 :::"up-complete"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "is" ($#v1_waybel_3 :::"compact"::: ) )) "holds" (Bool (Set (Var "y")) "is" ($#v1_waybel_3 :::"compact"::: ) )))) ; theorem :: WAYBEL_8:10 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "y"))))))) ; theorem :: WAYBEL_8:11 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Bool "not" (Set (Var "L1")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "L2")) "is" ($#v2_struct_0 :::"empty"::: ) ))) ; theorem :: WAYBEL_8:12 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v3_orders_2 :::"reflexive"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v3_orders_2 :::"reflexive"::: ) )) ; theorem :: WAYBEL_8:13 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v4_orders_2 :::"transitive"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v4_orders_2 :::"transitive"::: ) )) ; theorem :: WAYBEL_8:14 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) )) ; theorem :: WAYBEL_8:15 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v24_waybel_0 :::"up-complete"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v24_waybel_0 :::"up-complete"::: ) )) ; theorem :: WAYBEL_8:16 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v1_waybel_8 :::"satisfying_axiom_K"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" ) ")" )) "holds" (Bool (Set (Var "L2")) "is" ($#v1_waybel_8 :::"satisfying_axiom_K"::: ) )) ; theorem :: WAYBEL_8:17 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) ; theorem :: WAYBEL_8:18 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v3_waybel_8 :::"arithmetic"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v3_waybel_8 :::"arithmetic"::: ) )) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v5_orders_2 :::"antisymmetric"::: ) ; end; registrationlet "L" be ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v2_lattice3 :::"with_infima"::: ) ; end; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v1_lattice3 :::"with_suprema"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v24_waybel_0 :::"up-complete"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v2_waybel_8 :::"algebraic"::: ) ; end; registrationlet "L" be ($#v3_waybel_8 :::"arithmetic"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" ) -> ($#v3_waybel_8 :::"arithmetic"::: ) ; end; theorem :: WAYBEL_8:19 (Bool "for" (Set (Var "L")) "being" ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_8 :::"arithmetic"::: ) ) "iff" (Bool (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L"))) "is" ($#l1_orders_2 :::"LATTICE":::)) ")" )) ; theorem :: WAYBEL_8:20 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_8 :::"arithmetic"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k1_waybel_4 :::"-waybelow"::: ) ) "is" ($#v5_waybel_7 :::"multiplicative"::: ) ) ")" )) ; theorem :: WAYBEL_8:21 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_8 :::"arithmetic"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_waybel_7 :::"pseudoprime"::: ) )) "holds" (Bool (Set (Var "p")) "is" ($#v5_waybel_6 :::"prime"::: ) ))) ; theorem :: WAYBEL_8:22 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_1 :::"distributive"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_waybel_7 :::"pseudoprime"::: ) )) "holds" (Bool (Set (Var "p")) "is" ($#v5_waybel_6 :::"prime"::: ) ) ")" )) "holds" (Bool (Set (Var "L")) "is" ($#v3_waybel_8 :::"arithmetic"::: ) )) ; registrationlet "L" be ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::); let "c" be ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L")) "," (Set (Const "L")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) "c" ")" ))); end; theorem :: WAYBEL_8:23 (Bool "for" (Set (Var "L")) "being" ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool (Set (Set (Var "c")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c")) ")" ) ")" ))))) ; theorem :: WAYBEL_8:24 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c"))) "is" ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::)))) ; theorem :: WAYBEL_8:25 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool (Set (Set (Var "c")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c")) ")" ) ")" ))))) ; begin theorem :: WAYBEL_8:26 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" )) "iff" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" )) ; theorem :: WAYBEL_8:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "Y"))))) "holds" (Bool "ex" (Set (Var "Z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "Z")))))) ")" ))) ; theorem :: WAYBEL_8:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ))) ; theorem :: WAYBEL_8:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "x")) : (Bool verum) "}" ))) ; theorem :: WAYBEL_8:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" ))) "iff" (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Const "X")) ")" ); cluster (Set ($#k2_waybel_8 :::"compactbelow"::: ) "x") -> ($#v1_waybel_0 :::"directed"::: ) ($#v12_waybel_0 :::"lower"::: ) ; end; theorem :: WAYBEL_8:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X"))) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_yellow_1 :::"BoolePoset"::: ) "X") -> ($#v2_waybel_8 :::"algebraic"::: ) ; end;