:: WAYBEL11 semantic presentation begin scheme :: WAYBEL11:sch 1 Irrel{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F3 "(" (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "u"))]) "}" ($#r1_hidden :::"="::: ) "{" (Set F4 "(" (Set (Var "i")) "," (Set (Var "v")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "v"))]) "}" ) provided (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F3 "(" (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "i")) "," (Set (Var "u")) ")" )))) proof end; theorem :: WAYBEL11:1 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Y")) ($#r4_yellow_4 :::"is_coarser_than"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )))) ; theorem :: WAYBEL11:2 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r3_yellow_4 :::"is_finer_than"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )))) ; theorem :: WAYBEL11:3 (Bool "for" (Set (Var "T")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v1_waybel_0 :::"directed"::: ) )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_waybel_0 :::"directed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: WAYBEL11:4 (Bool "for" (Set (Var "T")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))))) ; registration cluster ($#v8_struct_0 :::"finite"::: ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "T" be ($#v8_struct_0 :::"finite"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v12_waybel_0 :::"lower"::: ) ($#v13_waybel_0 :::"upper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; registrationlet "R" be (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v13_waybel_0 :::"upper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; theorem :: WAYBEL11:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))))))) ; theorem :: WAYBEL11:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "S" is :::"inaccessible_by_directed_joins"::: means :: WAYBEL11:def 1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Var "D")) ($#r1_xboole_0 :::"meets"::: ) "S")); attr "S" is :::"closed_under_directed_sups"::: means :: WAYBEL11:def 2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) "S")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) "S")); attr "S" is :::"property(S)"::: means :: WAYBEL11:def 3 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "S") ")" ) ")" ))); end; :: deftheorem defines :::"inaccessible_by_directed_joins"::: WAYBEL11:def 1 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel11 :::"inaccessible_by_directed_joins"::: ) ) "iff" (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 "T")) "st" (Bool (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "D")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"closed_under_directed_sups"::: WAYBEL11:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_waybel11 :::"closed_under_directed_sups"::: ) ) "iff" (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 "T")) "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"property(S)"::: WAYBEL11:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_waybel11 :::"property(S)"::: ) ) "iff" (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 "T")) "st" (Bool (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" ))) ")" ))); notationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); synonym :::"inaccessible"::: "S" for :::"inaccessible_by_directed_joins"::: ; synonym :::"directly_closed"::: "S" for :::"closed_under_directed_sups"::: ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_waybel11 :::"directly_closed"::: ) ($#v3_waybel11 :::"property(S)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v2_waybel11 :::"directly_closed"::: ) ($#v3_waybel11 :::"property(S)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#v3_waybel11 :::"property(S)"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "S" ($#k3_subset_1 :::"`"::: ) ) -> ($#v2_waybel11 :::"directly_closed"::: ) ; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) ; attr "T" is :::"Scott"::: means :: WAYBEL11:def 4 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel11 :::"inaccessible"::: ) ) & (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"Scott"::: WAYBEL11:def 4 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel11 :::"inaccessible"::: ) ) & (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ) ")" )) ")" )); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v1_waybel11 :::"inaccessible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) ; redefine attr "T" is :::"Scott"::: means :: WAYBEL11:def 5 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" )); end; :: deftheorem defines :::"Scott"::: WAYBEL11:def 5 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#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"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "T") -> ($#v1_waybel11 :::"inaccessible"::: ) ($#v2_waybel11 :::"directly_closed"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v12_waybel_0 :::"lower"::: ) ($#v13_waybel_0 :::"upper"::: ) ($#v1_waybel11 :::"inaccessible"::: ) ($#v2_waybel11 :::"directly_closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#v1_waybel11 :::"inaccessible"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "S" ($#k3_subset_1 :::"`"::: ) ) -> ($#v2_waybel11 :::"directly_closed"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#v2_waybel11 :::"directly_closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "S" ($#k3_subset_1 :::"`"::: ) ) -> ($#v1_waybel11 :::"inaccessible"::: ) ; end; theorem :: WAYBEL11:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_waybel11 :::"directly_closed"::: ) ) & (Bool (Set (Var "S")) "is" ($#v12_waybel_0 :::"lower"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL11:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) "is" ($#v2_waybel11 :::"directly_closed"::: ) ))) ; theorem :: WAYBEL11:9 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL11:10 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set (Var "T")) "is" ($#l1_pre_topc :::"T_0-TopSpace":::))) ; theorem :: WAYBEL11:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: WAYBEL11:12 (Bool "for" (Set (Var "T")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: WAYBEL11:13 (Bool "for" (Set (Var "T")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) ) "is" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "A")))))) ; theorem :: WAYBEL11:14 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")))) & (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" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "S"))) ")" ) ")" )))) ; theorem :: WAYBEL11:15 (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Var "S")) "is" ($#v3_waybel11 :::"property(S)"::: ) ) ")" ) ")" ))) ; registrationlet "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster ($#v12_waybel_0 :::"lower"::: ) -> ($#v3_waybel11 :::"property(S)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: WAYBEL11:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "S")) where S "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "S")) "is" ($#v3_waybel11 :::"property(S)"::: ) ) "}" )) "holds" (Bool (Set (Var "T")) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) )) ; begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "R")); func :::"lim_inf"::: "N" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: WAYBEL11:def 6 (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element":::) "of" "N" : (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) "}" "," "R" ")" ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" "N" : (Bool verum) "}" "," "R" ")" ); end; :: deftheorem defines :::"lim_inf"::: WAYBEL11:def 6 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool (Set (Var "i")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) "}" "," (Set (Var "R")) ")" ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool verum) "}" "," (Set (Var "R")) ")" )))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "R")); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); pred "p" :::"is_S-limit_of"::: "N" means :: WAYBEL11:def 7 (Bool "p" ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) "N")); end; :: deftheorem defines :::"is_S-limit_of"::: WAYBEL11:def 7 : (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 "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_waybel11 :::"is_S-limit_of"::: ) (Set (Var "N"))) "iff" (Bool (Set (Var "p")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))) ")" )))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"Scott-Convergence"::: "R" -> ($#m4_yellow_6 :::"Convergence-Class"::: ) "of" "R" means :: WAYBEL11:def 8 (Bool "for" (Set (Var "N")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"net":::) "of" "R" "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) "R"))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "p")) ($#r1_waybel11 :::"is_S-limit_of"::: ) (Set (Var "N"))) ")" ))); end; :: deftheorem defines :::"Scott-Convergence"::: WAYBEL11:def 8 : (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 "b2")) "being" ($#m4_yellow_6 :::"Convergence-Class"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel11 :::"Scott-Convergence"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "N")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "R"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "p")) ($#r1_waybel11 :::"is_S-limit_of"::: ) (Set (Var "N"))) ")" ))) ")" ))); theorem :: WAYBEL11:17 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "p")) ($#r1_waybel11 :::"is_S-limit_of"::: ) (Set (Var "N"))) & (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "p")) ($#r3_orders_2 :::"<="::: ) (Set (Var "q")))))) ; theorem :: WAYBEL11:18 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r1_orders_2 :::">="::: ) (Set (Var "q")))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "R")); redefine attr "N" is :::"monotone"::: means :: WAYBEL11:def 9 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r3_orders_2 :::"<="::: ) (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))))); end; :: deftheorem defines :::"monotone"::: WAYBEL11:def 9 : (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 "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v8_waybel_0 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))))) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); func :::"Net-Str"::: "(" "S" "," "f" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "R" means :: WAYBEL11:def 10 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "S") & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_funct_2 :::"="::: ) "f") & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" it "holds" (Bool "(" (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j"))) "iff" (Bool (Set it ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set it ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Net-Str"::: WAYBEL11:def 10 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" (Set (Var "S")) "," (Set (Var "f")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b4"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b4")) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j"))) "iff" (Bool (Set (Set (Var "b4")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "b4")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))) ")" ) ")" ) ")" ) ")" ))))); theorem :: WAYBEL11:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool verum) "}" ))) ; theorem :: WAYBEL11:20 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v1_waybel_0 :::"directed"::: ) )) "holds" (Bool (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" (Set (Var "S")) "," (Set (Var "f")) ")" ) "is" ($#v7_waybel_0 :::"directed"::: ) )))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); cluster (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" "S" "," "f" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#v8_waybel_0 :::"monotone"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); cluster (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" "S" "," "f" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); cluster (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" "S" "," "f" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; theorem :: WAYBEL11:21 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "st" (Bool (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" (Set (Var "S")) "," (Set (Var "f")) ")" ) "is" ($#v7_waybel_0 :::"directed"::: ) )) "holds" (Bool (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" (Set (Var "S")) "," (Set (Var "f")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "R"))))))) ; registrationlet "R" be ($#l1_orders_2 :::"LATTICE":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ($#v8_waybel_0 :::"monotone"::: ) for ($#l1_waybel_0 :::"NetStr"::: ) "over" "R"; end; theorem :: WAYBEL11:22 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v8_waybel_0 :::"monotone"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_2 :::"sup"::: ) (Set (Var "N")))))) ; theorem :: WAYBEL11:23 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#v1_yellow_6 :::"constant"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k4_yellow_6 :::"the_value_of"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))))) ; theorem :: WAYBEL11:24 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#v1_yellow_6 :::"constant"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k4_yellow_6 :::"the_value_of"::: ) (Set (Var "N"))) ($#r1_waybel11 :::"is_S-limit_of"::: ) (Set (Var "N"))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "e" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func :::"Net-Str"::: "e" -> ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "S" means :: WAYBEL11:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) "e" ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) "e" "," "e" ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k6_domain_1 :::"{"::: ) "e" ($#k6_domain_1 :::"}"::: ) ))) ")" ); end; :: deftheorem defines :::"Net-Str"::: WAYBEL11:def 11 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel11 :::"Net-Str"::: ) (Set (Var "e")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "e")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b3"))) ($#r1_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ))) ")" ) ")" )))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "e" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k4_waybel11 :::"Net-Str"::: ) "e") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ; end; theorem :: WAYBEL11:25 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_waybel11 :::"Net-Str"::: ) (Set (Var "e")) ")" ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "e")))))) ; theorem :: WAYBEL11:26 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_waybel11 :::"Net-Str"::: ) (Set (Var "e")) ")" ) "holds" (Bool (Set (Set "(" ($#k4_waybel11 :::"Net-Str"::: ) (Set (Var "e")) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "e")))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "e" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k4_waybel11 :::"Net-Str"::: ) "e") -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL11:27 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_waybel11 :::"Net-Str"::: ) (Set (Var "e"))) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )))) ; theorem :: WAYBEL11:28 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" ($#k4_waybel11 :::"Net-Str"::: ) (Set (Var "e")) ")" ))))) ; theorem :: WAYBEL11:29 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_waybel11 :::"Net-Str"::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "S")))))) ; theorem :: WAYBEL11:30 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "Z")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "Z")) ($#k2_waybel_0 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Z")) : (Bool (Set (Var "k")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) "}" "," (Set (Var "R")) ")" ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Z")) : (Bool verum) "}" )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "D")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "D")) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" )))) ; theorem :: WAYBEL11:31 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k2_waybel11 :::"Scott-Convergence"::: ) (Set (Var "L")) ")" ) ")" ))) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel11 :::"inaccessible"::: ) ) & (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL11:32 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (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 "T")) ")" )))) ; theorem :: WAYBEL11:33 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_waybel_9 :::"TopLattice":::) "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 "T")) ")" )))) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel11 :::"inaccessible"::: ) ) & (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL11:34 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_waybel_9 :::"TopLattice":::) "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 "T")) ")" )))) "holds" (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) )) ; registrationlet "R" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k2_waybel11 :::"Scott-Convergence"::: ) "R") -> ($#v4_yellow_6 :::"(CONSTANTS)"::: ) ; end; registrationlet "R" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k2_waybel11 :::"Scott-Convergence"::: ) "R") -> ($#v5_yellow_6 :::"(SUBNETS)"::: ) ; end; theorem :: WAYBEL11:35 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k5_yellow_6 :::"""::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "M")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"sigma"::: "L" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "L" equals :: WAYBEL11:def 12 (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k2_waybel11 :::"Scott-Convergence"::: ) "L" ")" ) ")" )); end; :: deftheorem defines :::"sigma"::: WAYBEL11:def 12 : (Bool "for" (Set (Var "L")) "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 "L"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k2_waybel11 :::"Scott-Convergence"::: ) (Set (Var "L")) ")" ) ")" )))); theorem :: WAYBEL11:36 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: WAYBEL11:37 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "T"))))) "holds" (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) )) ; registrationlet "R" be ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k2_waybel11 :::"Scott-Convergence"::: ) "R") -> ($#v8_yellow_6 :::"topological"::: ) ; end; theorem :: WAYBEL11:38 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "T"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel11 :::"is_S-limit_of"::: ) (Set (Var "N"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N")))) ")" )))) ; theorem :: WAYBEL11:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool (Set ($#k2_waybel11 :::"Scott-Convergence"::: ) (Set (Var "L"))) "is" ($#v7_yellow_6 :::"(ITERATED_LIMITS)"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; theorem :: WAYBEL11:40 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool (Set ($#k12_yellow_6 :::"Convergence"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel11 :::"Scott-Convergence"::: ) (Set (Var "T")))) ")" )) ; theorem :: WAYBEL11:41 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_waybel_6 :::"Open"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: WAYBEL11:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "S")))))) ; theorem :: WAYBEL11:43 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "p"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ))))) ; theorem :: WAYBEL11:44 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "{" (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "q")) ")" ) where q "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "q")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "p"))) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" ))) ; theorem :: WAYBEL11:45 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "{" (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) : (Bool verum) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))) ; theorem :: WAYBEL11:46 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v1_waybel_6 :::"Open"::: ) ) ")" ))) ; theorem :: WAYBEL11:47 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "p")))))) ; theorem :: WAYBEL11:48 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) : (Bool (Set ($#k2_waybel_3 :::"wayabove"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) "}" )))) ;