:: WAYBEL14 semantic presentation begin theorem :: WAYBEL14:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "G")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool "not" (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "G")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ) ")" )))) ")" ) ")" )))) ; theorem :: WAYBEL14:2 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "iff" (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ))) ; theorem :: WAYBEL14:3 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "y")) ")" ))))) ; theorem :: WAYBEL14:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set "(" (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "y")) ")" ))))) ; theorem :: WAYBEL14:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")) ")" ))))) ; theorem :: WAYBEL14:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X")) ")" ))))) ; theorem :: WAYBEL14:7 (Bool "for" (Set (Var "R")) "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")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) "iff" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")))) ")" ))) ; theorem :: WAYBEL14:8 (Bool "for" (Set (Var "R")) "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")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) "iff" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "y")))) ")" ))) ; theorem :: WAYBEL14:9 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ))) ")" ))) ; theorem :: WAYBEL14:10 (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"::: ) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) ; theorem :: WAYBEL14:11 (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"::: ) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) ; theorem :: WAYBEL14:12 (Bool "for" (Set (Var "P")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set "(" (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ))))) ; theorem :: WAYBEL14:13 (Bool "for" (Set (Var "P")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ))))) ; theorem :: WAYBEL14:14 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "l")) "is" ($#v6_waybel_6 :::"co-prime"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" "not" (Bool (Set (Var "l")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y")))) "or" (Bool (Set (Var "l")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) "or" (Bool (Set (Var "l")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) ")" )) ")" ))) ; theorem :: WAYBEL14:15 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) : (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) "}" )))) ; theorem :: WAYBEL14:16 (Bool "for" (Set (Var "P")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P")) : (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) "}" )))) ; registrationlet "L" be ($#l1_orders_2 :::"sup-Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k2_waybel_8 :::"compactbelow"::: ) "x") -> ($#v1_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL14:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#v3_yellow_8 :::"irreducible"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "V")) "is" ($#v5_waybel_6 :::"prime"::: ) )))) ; theorem :: WAYBEL14:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "y")))) ")" ))) ; theorem :: WAYBEL14:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v5_waybel_6 :::"prime"::: ) ) "iff" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" "not" (Bool (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) "or" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) "or" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )) ")" ))) ; theorem :: WAYBEL14:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v6_waybel_6 :::"co-prime"::: ) ) "iff" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))) "or" (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "or" (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) ")" ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T")) -> ($#v2_waybel_1 :::"distributive"::: ) ; end; theorem :: WAYBEL14:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L")) "being" ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Var "l"))) & (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "l")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "t")))))))) ; theorem :: WAYBEL14:22 (Bool "for" (Set (Var "L")) "being" ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" )) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; begin registrationlet "L" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k5_waybel11 :::"sigma"::: ) "L") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: WAYBEL14:23 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "L"))))) ; theorem :: WAYBEL14:24 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; theorem :: WAYBEL14:25 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "VV")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "for" (Set (Var "X")) "being" ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "VV")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )) "holds" (Bool (Set (Var "VV")) "is" ($#v1_waybel_0 :::"directed"::: ) )))) ; theorem :: WAYBEL14:26 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X"))) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x")))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "R")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "R")); attr "f" is :::"jointly_Scott-continuous"::: means :: WAYBEL14:def 1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k2_waybel11 :::"Scott-Convergence"::: ) "R" ")" )))) "holds" (Bool "ex" (Set (Var "ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "ft")) ($#r1_funct_2 :::"="::: ) "f") & (Bool (Set (Var "ft")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))); end; :: deftheorem defines :::"jointly_Scott-continuous"::: WAYBEL14:def 1 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "R")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_waybel14 :::"jointly_Scott-continuous"::: ) ) "iff" (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k2_waybel11 :::"Scott-Convergence"::: ) (Set (Var "R")) ")" )))) "holds" (Bool "ex" (Set (Var "ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "ft")) ($#r1_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "ft")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))) ")" ))); theorem :: WAYBEL14:27 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v6_waybel_6 :::"co-prime"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) & (Bool (Set (Var "X")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ) ")" )))) ; theorem :: WAYBEL14:28 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v5_waybel_6 :::"prime"::: ) ) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) ")" )))) ; theorem :: WAYBEL14:29 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k5_waybel_2 :::"sup_op"::: ) (Set (Var "L"))) "is" ($#v1_waybel14 :::"jointly_Scott-continuous"::: ) ) & (Bool (Set (Var "V")) "is" ($#v5_waybel_6 :::"prime"::: ) ) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) )))))) ; theorem :: WAYBEL14:30 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool (Set ($#k5_waybel_2 :::"sup_op"::: ) (Set (Var "L"))) "is" ($#v1_waybel14 :::"jointly_Scott-continuous"::: ) )) ; theorem :: WAYBEL14:31 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set ($#k5_waybel_2 :::"sup_op"::: ) (Set (Var "L"))) "is" ($#v1_waybel14 :::"jointly_Scott-continuous"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v4_yellow_8 :::"sober"::: ) )) ; theorem :: WAYBEL14:32 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "L")) "is" ($#v6_waybel_3 :::"locally-compact"::: ) ) & (Bool (Set (Var "L")) "is" ($#v4_yellow_8 :::"sober"::: ) ) & (Bool (Set (Var "L")) "is" ($#v2_yellow_8 :::"Baire"::: ) ) ")" )) ; theorem :: WAYBEL14:33 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )))) ; theorem :: WAYBEL14:34 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )) ")" )) "holds" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; theorem :: WAYBEL14:35 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ))))) ; theorem :: WAYBEL14:36 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; theorem :: WAYBEL14:37 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ))) ")" ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")))) ")" ) "}" "," (Set (Var "L")) ")" )))) ; theorem :: WAYBEL14:38 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (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 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X")) ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")))) ")" ) "}" "," (Set (Var "L")) ")" )) ")" )) "holds" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; theorem :: WAYBEL14:39 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ))) ")" ) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "ex" (Set (Var "VV")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "VV")))) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "VV")))) "holds" (Bool (Set (Var "W")) "is" ($#v6_waybel_6 :::"co-prime"::: ) ) ")" ) ")" ))) ")" )) ; theorem :: WAYBEL14:40 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool "(" (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "ex" (Set (Var "VV")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "VV")))) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "VV")))) "holds" (Bool (Set (Var "W")) "is" ($#v6_waybel_6 :::"co-prime"::: ) ) ")" ) ")" )) ")" ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" ) "iff" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v1_waybel_5 :::"completely-distributive"::: ) ) ")" )) ; theorem :: WAYBEL14:41 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v1_waybel_5 :::"completely-distributive"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) ) & (Bool (Set (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" ) ")" )) ; theorem :: WAYBEL14:42 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ))) "}" ))) ; theorem :: WAYBEL14:43 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ))) "}" ))) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "ex" (Set (Var "VV")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "VV")))) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "VV")))) "holds" (Bool (Set (Var "W")) "is" ($#v6_waybel_6 :::"co-prime"::: ) ) ")" ) ")" )) ")" ) ")" )) ; theorem :: WAYBEL14:44 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "ex" (Set (Var "VV")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "VV")))) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "VV")))) "holds" (Bool (Set (Var "W")) "is" ($#v6_waybel_6 :::"co-prime"::: ) ) ")" ) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ))) "}" ))) ; theorem :: WAYBEL14:45 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" ))) "}" ))) "holds" (Bool (Set (Var "L")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) ;