:: WAYBEL23 semantic presentation begin theorem :: WAYBEL23:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (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 "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ) ($#k8_subset_1 :::"/\"::: ) (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"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Const "L")) ")" ) ")" ); :: original: :::"union"::: redefine func :::"union"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "L"; end; theorem :: WAYBEL23:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "Y")))))) ; theorem :: WAYBEL23:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v8_yellow_0 :::"sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "Y")))))))) ; theorem :: WAYBEL23:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v8_yellow_0 :::"sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "Y")))))))) ; theorem :: WAYBEL23:5 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X")))))))) ; theorem :: WAYBEL23:6 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" ($#k11_waybel_0 :::"finsups"::: ) (Set "(" ($#k1_waybel23 :::"union"::: ) (Set (Var "X")) ")" ) ")" ))))) ; theorem :: WAYBEL23:7 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL23:8 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL23:9 (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 ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL23:10 (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 ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL23:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")))))))) ; theorem :: WAYBEL23:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")))))))) ; theorem :: WAYBEL23:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))))))) ; theorem :: WAYBEL23:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")))))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "S" is :::"meet-closed"::: means :: WAYBEL23:def 1 (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ); end; :: deftheorem defines :::"meet-closed"::: WAYBEL23:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel23 :::"meet-closed"::: ) ) "iff" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "S" is :::"join-closed"::: means :: WAYBEL23:def 2 (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") "is" ($#v6_yellow_0 :::"join-inheriting"::: ) ); end; :: deftheorem defines :::"join-closed"::: WAYBEL23:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_waybel23 :::"join-closed"::: ) ) "iff" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))) "is" ($#v6_yellow_0 :::"join-inheriting"::: ) ) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "S" is :::"infs-closed"::: means :: WAYBEL23:def 3 (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ); end; :: deftheorem defines :::"infs-closed"::: WAYBEL23:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_waybel23 :::"infs-closed"::: ) ) "iff" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "S" is :::"sups-closed"::: means :: WAYBEL23:def 4 (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ); end; :: deftheorem defines :::"sups-closed"::: WAYBEL23:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_waybel23 :::"sups-closed"::: ) ) "iff" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v3_waybel23 :::"infs-closed"::: ) -> ($#v1_waybel23 :::"meet-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); cluster ($#v4_waybel23 :::"sups-closed"::: ) -> ($#v2_waybel23 :::"join-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_waybel23 :::"infs-closed"::: ) ($#v4_waybel23 :::"sups-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; theorem :: WAYBEL23:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel23 :::"meet-closed"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))) ; theorem :: WAYBEL23:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_waybel23 :::"join-closed"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))) ; theorem :: WAYBEL23:17 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel23 :::"meet-closed"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))) ; theorem :: WAYBEL23:18 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_waybel23 :::"join-closed"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))) ; theorem :: WAYBEL23:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_waybel23 :::"infs-closed"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))) ; theorem :: WAYBEL23:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_waybel23 :::"sups-closed"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))) ; theorem :: WAYBEL23:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_waybel23 :::"infs-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: WAYBEL23:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_waybel23 :::"sups-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: WAYBEL23:23 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel23 :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")))) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: WAYBEL23:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")))) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: WAYBEL23:25 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel23 :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))) "is" ($#v2_lattice3 :::"with_infima"::: ) ))) ; theorem :: WAYBEL23:26 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))) "is" ($#v1_lattice3 :::"with_suprema"::: ) ))) ; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel23 :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") -> ($#v2_lattice3 :::"with_infima"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") -> ($#v1_lattice3 :::"with_suprema"::: ) ; end; theorem :: WAYBEL23:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_waybel23 :::"infs-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))))) ; theorem :: WAYBEL23:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_waybel23 :::"sups-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))))) ; theorem :: WAYBEL23:29 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#v1_waybel23 :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "S")) "is" ($#v2_waybel_0 :::"filtered"::: ) ))) ; theorem :: WAYBEL23:30 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "S")) "is" ($#v1_waybel_0 :::"directed"::: ) ))) ; registrationlet "L" be ($#l1_orders_2 :::"Semilattice":::); cluster ($#v1_waybel23 :::"meet-closed"::: ) -> ($#v2_waybel_0 :::"filtered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#l1_orders_2 :::"sup-Semilattice":::); cluster ($#v2_waybel23 :::"join-closed"::: ) -> ($#v1_waybel_0 :::"directed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; theorem :: WAYBEL23:31 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))) "iff" (Bool (Set (Var "S")) "is" ($#v1_waybel23 :::"meet-closed"::: ) ) ")" ))) ; theorem :: WAYBEL23:32 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L"))) "iff" (Bool (Set (Var "S")) "is" ($#v2_waybel23 :::"join-closed"::: ) ) ")" ))) ; theorem :: WAYBEL23:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "S1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S2"))) "is" ($#v2_waybel23 :::"join-closed"::: ) ))) ; theorem :: WAYBEL23:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#v1_waybel23 :::"meet-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "S1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S2"))) "is" ($#v1_waybel23 :::"meet-closed"::: ) ))) ; theorem :: WAYBEL23:35 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) "is" ($#v2_waybel23 :::"join-closed"::: ) ))) ; theorem :: WAYBEL23:36 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) "is" ($#v1_waybel23 :::"meet-closed"::: ) ))) ; theorem :: WAYBEL23:37 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) "is" ($#v2_waybel23 :::"join-closed"::: ) ))) ; theorem :: WAYBEL23:38 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) "is" ($#v1_waybel23 :::"meet-closed"::: ) ))) ; registrationlet "L" be ($#l1_orders_2 :::"sup-Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k5_waybel_0 :::"downarrow"::: ) "x") -> ($#v2_waybel23 :::"join-closed"::: ) ; cluster (Set ($#k6_waybel_0 :::"uparrow"::: ) "x") -> ($#v2_waybel23 :::"join-closed"::: ) ; end; registrationlet "L" be ($#l1_orders_2 :::"Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k5_waybel_0 :::"downarrow"::: ) "x") -> ($#v1_waybel23 :::"meet-closed"::: ) ; cluster (Set ($#k6_waybel_0 :::"uparrow"::: ) "x") -> ($#v1_waybel23 :::"meet-closed"::: ) ; end; theorem :: WAYBEL23:39 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x"))) "is" ($#v2_waybel23 :::"join-closed"::: ) ))) ; theorem :: WAYBEL23:40 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x"))) "is" ($#v1_waybel23 :::"meet-closed"::: ) ))) ; theorem :: WAYBEL23:41 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x"))) "is" ($#v2_waybel23 :::"join-closed"::: ) ))) ; registrationlet "L" be ($#l1_orders_2 :::"sup-Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k1_waybel_3 :::"waybelow"::: ) "x") -> ($#v2_waybel23 :::"join-closed"::: ) ; cluster (Set ($#k2_waybel_3 :::"wayabove"::: ) "x") -> ($#v2_waybel23 :::"join-closed"::: ) ; end; registrationlet "L" be ($#l1_orders_2 :::"Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k1_waybel_3 :::"waybelow"::: ) "x") -> ($#v1_waybel23 :::"meet-closed"::: ) ; end; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; func :::"weight"::: "T" -> ($#m1_hidden :::"Cardinal":::) equals :: WAYBEL23:def 5 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k1_card_1 :::"card"::: ) (Set (Var "B")) ")" ) where B "is" ($#m1_subset_1 :::"Basis":::) "of" "T" : (Bool verum) "}" ); end; :: deftheorem defines :::"weight"::: WAYBEL23:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k1_card_1 :::"card"::: ) (Set (Var "B")) ")" ) where B "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) : (Bool verum) "}" ))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"second-countable"::: means :: WAYBEL23:def 6 (Bool (Set ($#k2_waybel23 :::"weight"::: ) "T") ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )); end; :: deftheorem defines :::"second-countable"::: WAYBEL23:def 6 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v5_waybel23 :::"second-countable"::: ) ) "iff" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )); definitionlet "L" be ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); mode :::"CLbasis"::: "of" "L" -> ($#m1_subset_1 :::"Subset":::) "of" "L" means :: WAYBEL23:def 7 (Bool "(" (Bool it "is" ($#v2_waybel23 :::"join-closed"::: ) ) & (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 "(" (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) it ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"CLbasis"::: WAYBEL23:def 7 : (Bool "for" (Set (Var "L")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L"))) "iff" (Bool "(" (Bool (Set (Var "b2")) "is" ($#v2_waybel23 :::"join-closed"::: ) ) & (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 "(" (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b2")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "S" is :::"with_bottom"::: means :: WAYBEL23:def 8 (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) "L") ($#r2_hidden :::"in"::: ) "S"); end; :: deftheorem defines :::"with_bottom"::: WAYBEL23:def 8 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_waybel23 :::"with_bottom"::: ) ) "iff" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "S" is :::"with_top"::: means :: WAYBEL23:def 9 (Bool (Set ($#k4_yellow_0 :::"Top"::: ) "L") ($#r2_hidden :::"in"::: ) "S"); end; :: deftheorem defines :::"with_top"::: WAYBEL23:def 9 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_waybel23 :::"with_top"::: ) ) "iff" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v6_waybel23 :::"with_bottom"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v7_waybel23 :::"with_top"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v6_waybel23 :::"with_bottom"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); cluster ($#v7_waybel23 :::"with_top"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster ($#v6_waybel23 :::"with_bottom"::: ) for ($#m1_waybel23 :::"CLbasis"::: ) "of" "L"; cluster ($#v7_waybel23 :::"with_top"::: ) for ($#m1_waybel23 :::"CLbasis"::: ) "of" "L"; end; theorem :: WAYBEL23:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") -> ($#v1_yellow_0 :::"lower-bounded"::: ) ; end; registrationlet "L" be ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster -> ($#v2_waybel23 :::"join-closed"::: ) for ($#m1_waybel23 :::"CLbasis"::: ) "of" "L"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#v3_yellow_0 :::"bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v2_waybel_3 :::"satisfying_axiom_of_approximation"::: ) ($#v3_waybel_3 :::"continuous"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_waybel23 :::"CLbasis"::: ) "of" "L"; end; theorem :: WAYBEL23:43 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )) "is" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")))) ; theorem :: WAYBEL23:44 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )) "is" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")))) ; theorem :: WAYBEL23:45 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )) "is" ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")))) "holds" (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) ; theorem :: WAYBEL23:46 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "B")) "being" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) ")" ))) ")" ))) ; theorem :: WAYBEL23:47 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "B")) "being" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L"))) "iff" (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 "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) ")" ))) ")" ))) ; theorem :: WAYBEL23:48 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "B")) "being" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) ")" )) ")" ) ")" ) ")" ))) ; theorem :: WAYBEL23:49 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "B")) "being" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Bool "not" (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) ")" ))) ")" ))) ; theorem :: WAYBEL23:50 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "is" ($#v2_waybel23 :::"join-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S")))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); func :::"supMap"::: "S" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "S" ")" ) ")" ) "," "L" means :: WAYBEL23:def 10 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "I")) "," "L" ")" ))); end; :: deftheorem defines :::"supMap"::: WAYBEL23:def 10 : (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "S")) ")" ) ")" ) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel23 :::"supMap"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "I")) "," (Set (Var "L")) ")" ))) ")" )))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); func :::"idsMap"::: "S" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "S" ")" ) ")" ) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ")" ) means :: WAYBEL23:def 11 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" "S" (Bool "ex" (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Var "J"))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "J")))) ")" ))); end; :: deftheorem defines :::"idsMap"::: WAYBEL23:def 11 : (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "S")) ")" ) ")" ) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel23 :::"idsMap"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Var "J"))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "J")))) ")" ))) ")" )))); registrationlet "L" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "B") -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "B") -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "B") -> ($#v5_orders_2 :::"antisymmetric"::: ) ; end; definitionlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "B" be ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Const "L")); func :::"baseMap"::: "B" -> ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "B" ")" ) ")" ) ")" ) means :: WAYBEL23:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) "B"))); end; :: deftheorem defines :::"baseMap"::: WAYBEL23:def 12 : (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))))) ")" )))); theorem :: WAYBEL23:51 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k3_waybel23 :::"supMap"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k3_waybel23 :::"supMap"::: ) (Set (Var "S")) ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))) ")" ))) ; theorem :: WAYBEL23:52 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k3_waybel23 :::"supMap"::: ) (Set (Var "S")) ")" ))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S"))) ")" )))) ; theorem :: WAYBEL23:53 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k4_waybel23 :::"idsMap"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_waybel23 :::"idsMap"::: ) (Set (Var "S")) ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" )) ")" ))) ; theorem :: WAYBEL23:54 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k4_waybel23 :::"idsMap"::: ) (Set (Var "S")) ")" ))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S"))) ")" )))) ; theorem :: WAYBEL23:55 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_waybel23 :::"idsMap"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")))))) ; theorem :: WAYBEL23:56 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B")) ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) ")" )) ")" ))) ; theorem :: WAYBEL23:57 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ))))) ; theorem :: WAYBEL23:58 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel23 :::"supMap"::: ) (Set (Var "S"))) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; theorem :: WAYBEL23:59 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel23 :::"idsMap"::: ) (Set (Var "S"))) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; theorem :: WAYBEL23:60 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B"))) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); cluster (Set ($#k3_waybel23 :::"supMap"::: ) "S") -> ($#v5_orders_3 :::"monotone"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); cluster (Set ($#k4_waybel23 :::"idsMap"::: ) "S") -> ($#v5_orders_3 :::"monotone"::: ) ; end; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "B" be ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Const "L")); cluster (Set ($#k5_waybel23 :::"baseMap"::: ) "B") -> ($#v5_orders_3 :::"monotone"::: ) ; end; theorem :: WAYBEL23:61 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel23 :::"idsMap"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" )) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ))) ; theorem :: WAYBEL23:62 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel23 :::"supMap"::: ) (Set (Var "S"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_waybel23 :::"idsMap"::: ) (Set (Var "S")) ")" ))))) ; theorem :: WAYBEL23:63 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set "(" ($#k3_waybel23 :::"supMap"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) ")" ) "," (Set "(" ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B")) ")" ) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ))) ; theorem :: WAYBEL23:64 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_waybel23 :::"supMap"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" )) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) ) & (Bool (Set ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B"))) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" ))) ; theorem :: WAYBEL23:65 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k3_waybel23 :::"supMap"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: WAYBEL23:66 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_waybel23 :::"supMap"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" )) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set ($#k3_waybel23 :::"supMap"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" )) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) ")" ))) ; theorem :: WAYBEL23:67 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_waybel23 :::"baseMap"::: ) (Set (Var "B"))) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "B" be ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Const "L")); cluster (Set ($#k3_waybel23 :::"supMap"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "B" ")" )) -> ($#v17_waybel_0 :::"infs-preserving"::: ) ($#v18_waybel_0 :::"sups-preserving"::: ) ; cluster (Set ($#k5_waybel23 :::"baseMap"::: ) "B") -> ($#v18_waybel_0 :::"sups-preserving"::: ) ; end; theorem :: WAYBEL23:68 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) : (Bool verum) "}" ))) ; theorem :: WAYBEL23:69 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) ")" ) ")" )) "," (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B"))) ($#r5_waybel_1 :::"are_isomorphic"::: ) ))) ; theorem :: WAYBEL23:70 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "B1"))) ")" )) "holds" (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) "holds" (Bool (Set (Var "J")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "J")) "," (Set (Var "L")) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))))))) ; theorem :: WAYBEL23:71 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )) "is" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L"))) & (Bool "(" "for" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ) ")" ) ")" )) ; theorem :: WAYBEL23:72 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "st" (Bool "for" (Set (Var "B1")) "being" ($#v6_waybel23 :::"with_bottom"::: ) ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "B1"))))) ")" )) ; theorem :: WAYBEL23:73 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "b")))))) ; theorem :: WAYBEL23:74 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "st" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T")))))) ;