:: WAYBEL30 semantic presentation begin theorem :: WAYBEL30:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "d")) ")" ) where d "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) : (Bool verum) "}" )))) ; theorem :: WAYBEL30:2 (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 "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "R")) ")" ) ")" ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "D"))) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R"))))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "R" ")" )) -> ($#v24_waybel_0 :::"up-complete"::: ) ; end; theorem :: WAYBEL30:3 (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 "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "R")) ")" ) ")" ) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "D")))))) ; theorem :: WAYBEL30:4 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "R")) ")" ) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "R")) ")" ) ")" ) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "x")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "d")) ")" ) where d "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) : (Bool verum) "}" ))))) ; registrationlet "R" be ($#l1_orders_2 :::"Semilattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "R" ")" )) -> ($#v1_waybel_2 :::"satisfying_MC"::: ) ; end; registrationlet "R" be (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v7_struct_0 :::"trivial"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; theorem :: WAYBEL30:5 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "A")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ))) "holds" (Bool (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "A"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ))))) ; theorem :: WAYBEL30:6 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "A")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ))) "holds" (Bool (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "A"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "N"))) "#)" ))))) ; theorem :: WAYBEL30:7 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ; registrationlet "A" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k2_waybel19 :::"lambda"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "S" be ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) "S" ")" )) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v3_lattice3 :::"complete"::: ) ; end; registrationlet "N" be ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) "N" ")" )) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v3_lattice3 :::"complete"::: ) ; cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k2_waybel19 :::"lambda"::: ) "N" ")" )) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v3_lattice3 :::"complete"::: ) ; end; theorem :: WAYBEL30:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "T"))) ($#r1_tarski :::"c="::: ) "{" (Set "(" (Set (Var "W")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "F")) ")" ) ")" ) where W, F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "T")))) & (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) "}" )) ; theorem :: WAYBEL30:9 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "N"))))) ; theorem :: WAYBEL30:10 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N"))))) ; theorem :: WAYBEL30:11 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "M"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) "#)" ))) "holds" (Bool (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N"))))) ; theorem :: WAYBEL30:12 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N")))) "iff" (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_waybel11 :::"Scott"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registration cluster ($#v7_struct_0 :::"trivial"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) -> ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) bbbadV3_YELLOW_0() ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) ($#v2_waybel_2 :::"meet-continuous"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) bbbadV3_YELLOW_0() ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) ($#v1_compts_1 :::"compact"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; scheme :: WAYBEL30:sch 1 EmptySch{ F1() -> ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::), F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F3 "(" (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) proof end; theorem :: WAYBEL30:13 (Bool "for" (Set (Var "N")) "being" ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_waybel11 :::"property(S)"::: ) )) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "A"))) "is" ($#v3_waybel11 :::"property(S)"::: ) ))) ; registrationlet "N" be ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_orders_2 :::"LATTICE":::); let "A" be ($#v3_waybel11 :::"property(S)"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "N")); cluster (Set ($#k4_waybel_0 :::"uparrow"::: ) "A") -> ($#v3_waybel11 :::"property(S)"::: ) ; end; theorem :: WAYBEL30:14 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N"))))) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S"))))))) ; theorem :: WAYBEL30:15 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "J"))) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "J"))) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: WAYBEL30:16 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "y")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "{" (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) : (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "J"))) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")))))))) ; theorem :: WAYBEL30:17 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "X")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) (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 ($#k1_tops_1 :::"Int"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "Y")))))))) ; theorem :: WAYBEL30:18 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "X")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) (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 ($#k2_pre_topc :::"Cl"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "Y")))))))) ; theorem :: WAYBEL30:19 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "LM")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "LN")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "N")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "LM")) "," (Set (Var "LN")) ($#k2_borsuk_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "N")) ($#k3_yellow_3 :::":]"::: ) )))))) ; theorem :: WAYBEL30:20 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "P")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "N")) ($#k3_yellow_3 :::":]"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "R")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "N")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "P"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Q")) "," (Set (Var "R")) ($#k2_borsuk_1 :::":]"::: ) )))))) ; theorem :: WAYBEL30:21 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; registrationlet "N" be ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); cluster (Set "x" ($#k4_waybel_1 :::""/\""::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: WAYBEL30:22 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "N")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool (Set (Var "N")) "is" ($#v2_yellow13 :::"topological_semilattice"::: ) )) ; theorem :: WAYBEL30:23 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "N")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v8_pre_topc :::"Hausdorff"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "N")) "," (Set (Var "N")) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))))) "holds" (Bool (Set (Var "X")) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" )) ; definitionlet "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "N")); func "X" :::"^0"::: -> ($#m1_subset_1 :::"Subset":::) "of" "N" equals :: WAYBEL30:def 1 "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element":::) "of" "N" : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "N" "st" (Bool (Bool (Set (Var "u")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))))) "holds" (Bool "X" ($#r1_xboole_0 :::"meets"::: ) (Set (Var "D")))) "}" ; end; :: deftheorem defines :::"^0"::: WAYBEL30:def 1 : (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "X")) ($#k1_waybel30 :::"^0"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "u")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "D")))) "}" ))); registrationlet "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "N")); cluster (Set "X" ($#k1_waybel30 :::"^0"::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: WAYBEL30:24 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "J")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_waybel30 :::"^0"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "J")) ($#k1_waybel30 :::"^0"::: ) )))) ; theorem :: WAYBEL30:25 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) ($#k1_waybel30 :::"^0"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL30:26 (Bool "for" (Set (Var "N")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "X")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k1_waybel30 :::"^0"::: ) )))) ; theorem :: WAYBEL30:27 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k1_waybel30 :::"^0"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k1_waybel30 :::"^0"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k1_waybel30 :::"^0"::: ) )))) ; theorem :: WAYBEL30:28 (Bool "for" (Set (Var "N")) "being" ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k1_waybel30 :::"^0"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "Y")) ($#k1_waybel30 :::"^0"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k1_waybel30 :::"^0"::: ) )))) ; theorem :: WAYBEL30:29 (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "F")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "F")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" )))) ; theorem :: WAYBEL30:30 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "N")) "is" ($#v2_waybel_2 :::"meet-continuous"::: ) ) & (Bool (Set (Var "N")) "is" ($#v8_pre_topc :::"Hausdorff"::: ) ) ")" ) ")" )) ; registration cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v3_waybel_3 :::"continuous"::: ) -> ($#v8_pre_topc :::"Hausdorff"::: ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) -> ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; definitionlet "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) ; attr "N" is :::"with_small_semilattices"::: means :: WAYBEL30:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "N" (Bool "ex" (Set (Var "J")) "being" ($#m1_yellow13 :::"basis"::: ) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "N" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "A"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) )))); attr "N" is :::"with_compact_semilattices"::: means :: WAYBEL30:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "N" (Bool "ex" (Set (Var "J")) "being" ($#m1_yellow13 :::"basis"::: ) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "N" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool "(" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "A"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_compts_1 :::"compact"::: ) ) ")" )))); attr "N" is :::"with_open_semilattices"::: means :: WAYBEL30:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "N" (Bool "ex" (Set (Var "J")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "N" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "A"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) )))); end; :: deftheorem defines :::"with_small_semilattices"::: WAYBEL30:def 2 : (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v1_waybel30 :::"with_small_semilattices"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "J")) "being" ($#m1_yellow13 :::"basis"::: ) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "A"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) )))) ")" )); :: deftheorem defines :::"with_compact_semilattices"::: WAYBEL30:def 3 : (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v2_waybel30 :::"with_compact_semilattices"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "J")) "being" ($#m1_yellow13 :::"basis"::: ) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool "(" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "A"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_compts_1 :::"compact"::: ) ) ")" )))) ")" )); :: deftheorem defines :::"with_open_semilattices"::: WAYBEL30:def 4 : (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_waybel30 :::"with_open_semilattices"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "J")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "A"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) )))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_waybel30 :::"with_open_semilattices"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_waybel30 :::"with_small_semilattices"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_waybel30 :::"with_compact_semilattices"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_waybel30 :::"with_small_semilattices"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_waybel30 :::"with_small_semilattices"::: ) ($#v3_waybel30 :::"with_open_semilattices"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_waybel30 :::"with_compact_semilattices"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v1_waybel19 :::"lower"::: ) ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; theorem :: WAYBEL30:31 (Bool "for" (Set (Var "N")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#v2_yellow13 :::"topological_semilattice"::: ) ($#l1_waybel_9 :::"TopPoset":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "C"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) )) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C")) ")" )) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ))) ; theorem :: WAYBEL30:32 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "J")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set (Var "W")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "S"))))) ")" ) "iff" (Bool (Set (Var "N")) "is" ($#v3_waybel30 :::"with_open_semilattices"::: ) ) ")" ))) ; theorem :: WAYBEL30:33 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S")))) ")" ) "}" ($#r1_tarski :::"c="::: ) "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "J")) ")" ) where J "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N")))) ")" ) "}" )))) ; theorem :: WAYBEL30:34 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S")))) ")" ) "}" ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "J")) ")" ) where J "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N")))) ")" ) "}" )))) ; theorem :: WAYBEL30:35 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_waybel30 :::"with_open_semilattices"::: ) ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "N")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" ) ")" )) ; registration cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v3_waybel_3 :::"continuous"::: ) -> ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v3_waybel30 :::"with_open_semilattices"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registrationlet "N" be ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) "N" ")" )) -> ($#v3_waybel_3 :::"continuous"::: ) ; end; theorem :: WAYBEL30:36 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "N")) "is" ($#v8_pre_topc :::"Hausdorff"::: ) ) & (Bool (Set (Var "N")) "is" ($#v2_yellow13 :::"topological_semilattice"::: ) ) & (Bool (Set (Var "N")) "is" ($#v3_waybel30 :::"with_open_semilattices"::: ) ) ")" )) ; theorem :: WAYBEL30:37 (Bool "for" (Set (Var "N")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_yellow13 :::"topological_semilattice"::: ) ($#v3_waybel30 :::"with_open_semilattices"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set (Var "N")) "is" ($#v2_waybel30 :::"with_compact_semilattices"::: ) )) ; theorem :: WAYBEL30:38 (Bool "for" (Set (Var "N")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "V")) ")" ) where V "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N")))) ")" ) "}" "," (Set (Var "N")) ")" )))) ; theorem :: WAYBEL30:39 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "V")) ")" ) where V "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "N")))) ")" ) "}" "," (Set (Var "N")) ")" ))) ")" )) ; theorem :: WAYBEL30:40 (Bool "for" (Set (Var "N")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_waybel30 :::"with_open_semilattices"::: ) ) & (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "N")) ")" )) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) ")" ) ")" )) ; registrationlet "N" be ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) "N" ")" )) -> ($#v2_waybel_8 :::"algebraic"::: ) ; end;