:: WAYBEL12 semantic presentation begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); redefine attr "P" is :::"closed"::: means :: WAYBEL12:def 1 (Bool (Set "P" ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ); end; :: deftheorem defines :::"closed"::: WAYBEL12:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "F" is :::"dense"::: means :: WAYBEL12:def 2 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "X")) "is" ($#v1_tops_1 :::"dense"::: ) )); end; :: deftheorem defines :::"dense"::: WAYBEL12:def 2 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_waybel12 :::"dense"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#v1_tops_1 :::"dense"::: ) )) ")" ))); theorem :: WAYBEL12:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y")))) & (Bool (Set (Var "Y")) "is" ($#v4_card_3 :::"countable"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v4_card_3 :::"countable"::: ) )) ; theorem :: WAYBEL12:2 (Bool "for" (Set (Var "A")) "being" ($#v5_card_3 :::"denumerable"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "A")) ($#r2_tarski :::"are_equipotent"::: ) )) ; theorem :: WAYBEL12: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 "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "B")))))) ; theorem :: WAYBEL12:4 (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 "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "B")))))) ; theorem :: WAYBEL12:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))))) ; theorem :: WAYBEL12:6 (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 "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: WAYBEL12:7 (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 "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL12:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: WAYBEL12:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL12:10 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "X")) ($#k4_yellow_4 :::""/\""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: WAYBEL12:11 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "X")) ($#k4_yellow_4 :::""/\""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: WAYBEL12:12 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "X")) ($#k2_yellow_4 :::""\/""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: WAYBEL12:13 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "X")) ($#k2_yellow_4 :::""\/""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: WAYBEL12:14 (Bool "for" (Set (Var "L")) "being" ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: WAYBEL12:15 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: WAYBEL12:16 (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 "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r3_yellow_4 :::"is_finer_than"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r4_yellow_4 :::"is_coarser_than"::: ) (Set (Var "B"))) ")" ))) ; theorem :: WAYBEL12:17 (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 "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "V"))) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "V"))))))) ; theorem :: WAYBEL12:18 (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 "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "V"))) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "V"))))))) ; theorem :: WAYBEL12:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "S")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "T"))) & (Bool (Set (Var "V")) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Var "T")) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))))) ; theorem :: WAYBEL12:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "S")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "T"))) & (Bool (Set (Var "V")) "is" ($#v12_waybel_0 :::"lower"::: ) ) & (Bool (Set (Var "T")) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))))) ; theorem :: WAYBEL12:21 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "F")) "being" ($#v2_waybel_0 :::"filtered"::: ) ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "F")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; theorem :: WAYBEL12:22 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "I")) "being" ($#v1_waybel_0 :::"directed"::: ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "I")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Var "I"))))) ; theorem :: WAYBEL12:23 (Bool "for" (Set (Var "L")) "being" ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Bool "not" "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "V")) ($#k4_yellow_4 :::""/\""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) "}" "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: WAYBEL12:24 (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 "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "V")) ($#k4_yellow_4 :::""/\""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) "}" "is" ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL12: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 "V")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "V")) ($#k4_yellow_4 :::""/\""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) "}" "is" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL12:26 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_waybel_6 :::"Open"::: ) ) & (Bool (Set (Var "X")) "is" ($#v12_waybel_0 :::"lower"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ))) ; registrationlet "L" be ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#v12_waybel_0 :::"lower"::: ) ($#v1_waybel_6 :::"Open"::: ) -> ($#v2_waybel_0 :::"filtered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v12_waybel_0 :::"lower"::: ) -> ($#v1_waybel_6 :::"Open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); end; registrationlet "L" be ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) "x" ")" ) ($#k3_subset_1 :::"`"::: ) ) -> ($#v1_waybel_6 :::"Open"::: ) ; end; theorem :: WAYBEL12:27 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (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 "C"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "y")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) ")" )) "holds" (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))))) ; theorem :: WAYBEL12:28 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (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 "C"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "y")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) ")" )) "holds" (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))))) ; definitionlet "L" be ($#l1_orders_2 :::"Semilattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); mode :::"GeneratorSet"::: "of" "F" -> ($#m1_subset_1 :::"Subset":::) "of" "L" means :: WAYBEL12:def 3 (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" ($#k12_waybel_0 :::"fininfs"::: ) it ")" ))); end; :: deftheorem defines :::"GeneratorSet"::: WAYBEL12:def 3 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_waybel12 :::"GeneratorSet"::: ) "of" (Set (Var "F"))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "b3")) ")" ))) ")" )))); registrationlet "L" be ($#l1_orders_2 :::"Semilattice":::); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_waybel12 :::"GeneratorSet"::: ) "of" "F"; end; theorem :: WAYBEL12:29 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) ($#r4_yellow_4 :::"is_coarser_than"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "A"))) ($#r4_yellow_4 :::"is_coarser_than"::: ) (Set ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "B"))))))) ; theorem :: WAYBEL12:30 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "G")) "being" ($#m1_waybel12 :::"GeneratorSet"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "G")) ($#r4_yellow_4 :::"is_coarser_than"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r4_yellow_4 :::"is_coarser_than"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_waybel12 :::"GeneratorSet"::: ) "of" (Set (Var "F"))))))) ; theorem :: WAYBEL12:31 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")) ")" ) where m "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" "," (Set (Var "L")) ")" )) ")" )) "holds" (Bool (Set (Var "A")) ($#r4_yellow_4 :::"is_coarser_than"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))))))) ; theorem :: WAYBEL12:32 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "G")) "being" ($#m1_waybel12 :::"GeneratorSet"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")) ")" ) where m "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" "," (Set (Var "L")) ")" )) ")" )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) "is" ($#m1_waybel12 :::"GeneratorSet"::: ) "of" (Set (Var "F"))))))) ; begin theorem :: WAYBEL12:33 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "V")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#v1_waybel_6 :::"Open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "V")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_waybel12 :::"GeneratorSet"::: ) "of" (Set (Var "F")) "st" (Bool (Set (Var "A")) "is" ($#v4_card_3 :::"countable"::: ) ))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#v1_waybel_6 :::"Open"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "O")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "O"))) ")" )))))) ; theorem :: WAYBEL12:34 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "V")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#v1_waybel_6 :::"Open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_card_3 :::"countable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "V")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#v1_waybel_6 :::"Open"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Var "O"))) & (Bool (Set (Var "O")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) ")" )))))) ; theorem :: WAYBEL12:35 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "V")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#v1_waybel_6 :::"Open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_card_3 :::"countable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "V")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#v2_waybel_6 :::"irreducible"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "p"))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "N")) ")" )))) ")" )))))) ; theorem :: WAYBEL12:36 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_card_3 :::"countable"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "," (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")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool "not" (Bool (Set (Set (Var "y")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "n"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "x")))) ")" )) "holds" (Bool "for" (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 "p")) "being" ($#v2_waybel_6 :::"irreducible"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "p"))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "N")) ")" )))) ")" )))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "u" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); attr "u" is :::"dense"::: means :: WAYBEL12:def 4 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "L"))) "holds" (Bool (Set "u" ($#k11_lattice3 :::""/\""::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "L"))); end; :: deftheorem defines :::"dense"::: WAYBEL12:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "u")) "is" ($#v2_waybel12 :::"dense"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "u")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) ")" ))); registrationlet "L" be ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::); cluster (Set ($#k4_yellow_0 :::"Top"::: ) "L") -> ($#v2_waybel12 :::"dense"::: ) ; end; registrationlet "L" be ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::); cluster ($#v2_waybel12 :::"dense"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"); end; theorem :: WAYBEL12:37 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v3_yellow_0 :::"bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v2_waybel12 :::"dense"::: ) )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "D" is :::"dense"::: means :: WAYBEL12:def 5 (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set (Var "d")) "is" ($#v2_waybel12 :::"dense"::: ) )); end; :: deftheorem defines :::"dense"::: WAYBEL12:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#v3_waybel12 :::"dense"::: ) ) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "d")) "is" ($#v2_waybel12 :::"dense"::: ) )) ")" ))); theorem :: WAYBEL12:38 (Bool "for" (Set (Var "L")) "being" ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v3_waybel12 :::"dense"::: ) )) ; registrationlet "L" be ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) ($#v3_waybel12 :::"dense"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); end; theorem :: WAYBEL12:39 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_card_3 :::"countable"::: ) ($#v3_waybel12 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#v2_waybel_6 :::"irreducible"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D")) ")" )))) ")" ))))) ; theorem :: WAYBEL12:40 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_yellow_8 :::"irreducible"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v2_waybel_6 :::"irreducible"::: ) )))) ; theorem :: WAYBEL12:41 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" )))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_waybel_6 :::"irreducible"::: ) ) "iff" (Bool (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_yellow_8 :::"irreducible"::: ) ) ")" )))) ; theorem :: WAYBEL12:42 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_waybel12 :::"dense"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" )))) ; theorem :: WAYBEL12:43 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v6_waybel_3 :::"locally-compact"::: ) )) "holds" (Bool "for" (Set (Var "D")) "being" ($#v4_card_3 :::"countable"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "D")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "D")) "is" ($#v1_waybel12 :::"dense"::: ) ) & (Bool (Set (Var "D")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "O")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "A")) "being" ($#v3_yellow_8 :::"irreducible"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_finsub_1 :::"/\"::: ) (Set (Var "O"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "V")))))))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); redefine attr "T" is :::"Baire"::: means :: WAYBEL12:def 6 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) ) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool (Set (Var "I")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))); end; :: deftheorem defines :::"Baire"::: WAYBEL12:def 6 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v2_yellow_8 :::"Baire"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) ) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool (Set (Var "I")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))) ")" )); theorem :: WAYBEL12:44 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v4_yellow_8 :::"sober"::: ) ) & (Bool (Set (Var "T")) "is" ($#v6_waybel_3 :::"locally-compact"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v2_yellow_8 :::"Baire"::: ) )) ;