:: WAYBEL31 semantic presentation begin scheme :: WAYBEL31:sch 1 UparrowUnion{ F1() -> ($#l1_orders_2 :::"RelStr"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" )) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" ))) proof end; scheme :: WAYBEL31:sch 2 DownarrowUnion{ F1() -> ($#l1_orders_2 :::"RelStr"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" )) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" ))) proof end; registrationlet "L1" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "B1" be ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Const "L1")); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "B1" ")" ) ")" )) -> ($#v2_waybel_8 :::"algebraic"::: ) ; end; definitionlet "L1" be ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); func :::"CLweight"::: "L1" -> ($#m1_hidden :::"Cardinal":::) equals :: WAYBEL31:def 1 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k1_card_1 :::"card"::: ) (Set (Var "B1")) ")" ) where B1 "is" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" "L1" : (Bool verum) "}" ); end; :: deftheorem defines :::"CLweight"::: WAYBEL31:def 1 : (Bool "for" (Set (Var "L1")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k1_card_1 :::"card"::: ) (Set (Var "B1")) ")" ) where B1 "is" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) : (Bool verum) "}" ))); theorem :: WAYBEL31:1 (Bool "for" (Set (Var "L1")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B1")))))) ; theorem :: WAYBEL31:2 (Bool "for" (Set (Var "L1")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "ex" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "st" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1")))))) ; theorem :: WAYBEL31:3 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L1")) ")" ))))) ; theorem :: WAYBEL31:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L1")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) ($#r1_hidden :::"="::: ) (Set (Var "L1")))) "holds" (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "holds" (Bool (Set (Var "B1")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))))) ; theorem :: WAYBEL31:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) ($#r1_hidden :::"="::: ) (Set (Var "L1")))) "holds" (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "B2"))) "is" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1"))))))) ; theorem :: WAYBEL31:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) ($#r1_hidden :::"="::: ) (Set (Var "L1"))) & (Bool (Set (Var "T")) "is" ($#v8_struct_0 :::"infinite"::: ) )) "holds" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1")))))) ; theorem :: WAYBEL31:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L1")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) ($#r1_hidden :::"="::: ) (Set (Var "L1")))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))))))) ; theorem :: WAYBEL31:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))))) ; theorem :: WAYBEL31:9 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) ($#r1_hidden :::"="::: ) (Set (Var "L1"))) & (Bool (Set (Var "T")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))))))) ; theorem :: WAYBEL31:10 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "T1")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L1")) (Bool "for" (Set (Var "T2")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T2")) "holds" (Bool "{" (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "V")) ")" ) where V "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")) : (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B2"))) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T1"))))))) ; theorem :: WAYBEL31:11 (Bool "for" (Set (Var "L1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel_8 :::"compactbelow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL31:12 (Bool "for" (Set (Var "L1")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set (Var "L1")) "is" ($#v3_waybel_8 :::"arithmetic"::: ) )) ; registration cluster ($#v8_struct_0 :::"finite"::: ) ($#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 ($#v8_struct_0 :::"finite"::: ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: WAYBEL31:13 (Bool "for" (Set (Var "L1")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "holds" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1")))) "iff" (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L1")) ")" ))) ")" ))) ; definitionlet "L1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L1")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L1")); func :::"Way_Up"::: "(" "a" "," "A" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "L1" equals :: WAYBEL31:def 2 (Set (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) "a" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) "A" ")" )); end; :: deftheorem defines :::"Way_Up"::: WAYBEL31:def 2 : (Bool "for" (Set (Var "L1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set ($#k2_waybel31 :::"Way_Up"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "a")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "A")) ")" )))))); theorem :: WAYBEL31:14 (Bool "for" (Set (Var "L1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set ($#k2_waybel31 :::"Way_Up"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "L1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "a")))))) ; theorem :: WAYBEL31:15 (Bool "for" (Set (Var "L1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k2_waybel31 :::"Way_Up"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: WAYBEL31:16 (Bool "for" (Set (Var "L1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L1"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: WAYBEL31:17 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v8_struct_0 :::"infinite"::: ) )) "holds" (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "holds" (Bool (Set (Var "B1")) "is" ($#v1_finset_1 :::"infinite"::: ) ))) ; theorem :: WAYBEL31:18 (Bool "for" (Set (Var "L1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_waybel_3 :::"compact"::: ) )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ))))) ; theorem :: WAYBEL31:19 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v8_struct_0 :::"infinite"::: ) )) "holds" (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set "(" ($#k2_waybel31 :::"Way_Up"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")), A "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B1"))) ")" ) "}" ) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B1")))))) ; theorem :: WAYBEL31:20 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")) ")" ) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")) ")" ) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; theorem :: WAYBEL31:21 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L1")) (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "holds" (Bool "{" (Set "(" ($#k2_waybel31 :::"Way_Up"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")), A "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B1"))) ")" ) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))))) ; theorem :: WAYBEL31:22 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L1")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds" (Bool "{" (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "u")) ")" ) ")" ) where u "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))))) ; theorem :: WAYBEL31:23 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L1")) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B1")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) "}" "is" ($#v1_finset_1 :::"infinite"::: ) )))) ; theorem :: WAYBEL31:24 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L1")) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T")))))) ; theorem :: WAYBEL31:25 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L1")) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T")))))) ; theorem :: WAYBEL31:26 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1")))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2")))))) ; theorem :: WAYBEL31:27 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L1")) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))))) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel31 :::"CLweight"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B1")) ")" ) ")" ) ")" ))))) ; registrationlet "L1" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) "L1" ")" )) -> ($#v1_lattice3 :::"with_suprema"::: ) ($#v3_waybel_3 :::"continuous"::: ) ; end; theorem :: WAYBEL31:28 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_waybel31 :::"CLweight"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L1")) ")" ) ")" )))) ; theorem :: WAYBEL31:29 (Bool "for" (Set (Var "L1")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "st" (Bool (Bool (Set (Var "L1")) "is" ($#v8_struct_0 :::"infinite"::: ) )) "holds" (Bool (Set ($#k1_waybel31 :::"CLweight"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel31 :::"CLweight"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L1")) ")" ) ")" )))) ;