:: WAYBEL32 semantic presentation begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) ; attr "T" is :::"upper"::: means :: WAYBEL32:def 1 (Bool "{" (Set "(" (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" "T" : (Bool verum) "}" "is" ($#m1_subset_1 :::"prebasis":::) "of" "T"); end; :: deftheorem defines :::"upper"::: WAYBEL32:def 1 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_waybel32 :::"upper"::: ) ) "iff" (Bool "{" (Set "(" (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) : (Bool verum) "}" "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))) ")" )); 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_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) ; attr "T" is :::"order_consistent"::: means :: WAYBEL32:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" "holds" (Bool "(" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool "(" "for" (Set (Var "N")) "being" ($#v10_waybel_0 :::"eventually-directed"::: ) ($#l1_waybel_0 :::"net":::) "of" "T" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_2 :::"sup"::: ) (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "V")))) ")" ) ")" )); end; :: deftheorem defines :::"order_consistent"::: WAYBEL32:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v2_waybel32 :::"order_consistent"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool "(" "for" (Set (Var "N")) "being" ($#v10_waybel_0 :::"eventually-directed"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_2 :::"sup"::: ) (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "V")))) ")" ) ")" )) ")" )); registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v1_waybel32 :::"upper"::: ) 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"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v1_waybel32 :::"upper"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; theorem :: WAYBEL32:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v1_waybel32 :::"upper"::: ) ($#l1_waybel_9 :::"TopPoset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v13_waybel_0 :::"upper"::: ) ))) ; theorem :: WAYBEL32:2 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_waybel_9 :::"TopPoset":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_waybel32 :::"upper"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v2_waybel32 :::"order_consistent"::: ) )) ; theorem :: WAYBEL32:3 (Bool "for" (Set (Var "R")) "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_orders_2 :::"RelStr"::: ) (Bool "ex" (Set (Var "T")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) "st" (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) ))) ; theorem :: WAYBEL32:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v2_pre_topc :::"correct"::: ) ))) ; registrationlet "R" be ($#~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_orders_2 :::"RelStr"::: ) ; cluster ($#v4_waybel11 :::"Scott"::: ) -> ($#v2_pre_topc :::"correct"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; registrationlet "R" be ($#~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_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"correct"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; theorem :: WAYBEL32:5 (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 ($#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 :: WAYBEL32:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopPoset":::) "holds" (Bool (Set (Var "T")) "is" ($#v2_waybel32 :::"order_consistent"::: ) )) ; theorem :: WAYBEL32:7 (Bool "for" (Set (Var "R")) "being" ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (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 :: WAYBEL32:8 (Bool "for" (Set (Var "R")) "being" ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "S")) "," (Set (Var "R")) ")" ) ($#r3_orders_2 :::"<="::: ) (Set (Var "a")))))) ; theorem :: WAYBEL32:9 (Bool "for" (Set (Var "R")) "being" ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (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 :: WAYBEL32:10 (Bool "for" (Set (Var "R")) "being" ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "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 "R")) ")" ) ")" ))) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_waybel11 :::"inaccessible"::: ) ) & (Bool (Set (Var "S")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL32:11 (Bool "for" (Set (Var "R")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) ))) ; registrationlet "R" be ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"correct"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; theorem :: WAYBEL32:12 (Bool "for" (Set (Var "S")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))))) ; theorem :: WAYBEL32:13 (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"::: ) "holds" (Bool (Set (Var "T")) "is" ($#l1_pre_topc :::"T_0-TopSpace":::))) ; registrationlet "R" be ($#~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_orders_2 :::"RelStr"::: ) ; cluster -> ($#v24_waybel_0 :::"up-complete"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; theorem :: WAYBEL32:14 (Bool "for" (Set (Var "R")) "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_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) (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 :: WAYBEL32:15 (Bool "for" (Set (Var "R")) "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 "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) (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 :: WAYBEL32:16 (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 "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)"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL32:17 (Bool "for" (Set (Var "R")) "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 "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "S")) "," (Set (Var "R")) ")" ))))) ; registrationlet "T" be ($#~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"::: ) ; 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 :: WAYBEL32:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "S")) "is" ($#v1_waybel11 :::"inaccessible"::: ) ))) ; theorem :: WAYBEL32:19 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) (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 :: WAYBEL32:20 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) (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")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) "or" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) : (Bool verum) "}" ) ")" ) ")" )))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"correct"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v2_waybel32 :::"order_consistent"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; 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_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel32 :::"order_consistent"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; theorem :: WAYBEL32:21 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) ")" ) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v13_waybel_0 :::"upper"::: ) ))) ; theorem :: WAYBEL32:22 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) ")" )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v12_waybel_0 :::"lower"::: ) )))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); func "R" :::"*'"::: "f" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "S" means :: WAYBEL32:def 3 (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_funct_2 :::"="::: ) "f") ")" ); end; :: deftheorem defines :::"*'"::: WAYBEL32:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (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 "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k1_waybel32 :::"*'"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b4"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b4"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f"))) ")" ) ")" ))))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set "R" ($#k1_waybel32 :::"*'"::: ) "f") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set "R" ($#k1_waybel32 :::"*'"::: ) "f") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#l1_waybel_0 :::"prenet":::) "of" (Set (Const "R")); func :::"inf_net"::: "N" -> ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"prenet":::) "of" "R" means :: WAYBEL32:def 4 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "N" "," "R" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set "N" ($#k1_waybel32 :::"*'"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "holds" (Bool (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element":::) "of" "N" : (Bool (Set (Var "k")) ($#r1_orders_2 :::">="::: ) (Set (Var "i"))) "}" "," "R" ")" )) ")" ) ")" )); end; :: deftheorem defines :::"inf_net"::: WAYBEL32:def 4 : (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 :::"prenet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"prenet":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel32 :::"inf_net"::: ) (Set (Var "N")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k1_waybel32 :::"*'"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool (Set (Var "k")) ($#r1_orders_2 :::">="::: ) (Set (Var "i"))) "}" "," (Set (Var "R")) ")" )) ")" ) ")" )) ")" )))); registrationlet "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")); cluster (Set ($#k2_waybel32 :::"inf_net"::: ) "N") -> ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "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")); cluster (Set ($#k2_waybel32 :::"inf_net"::: ) "N") -> ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "R")); cluster (Set ($#k2_waybel32 :::"inf_net"::: ) "N") -> ($#v6_waybel_0 :::"strict"::: ) ($#v8_waybel_0 :::"monotone"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "R")); cluster (Set ($#k2_waybel32 :::"inf_net"::: ) "N") -> ($#v6_waybel_0 :::"strict"::: ) ($#v10_waybel_0 :::"eventually-directed"::: ) ; end; theorem :: WAYBEL32:23 (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 ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set "(" ($#k2_waybel32 :::"inf_net"::: ) (Set (Var "N")) ")" ))) ($#r1_hidden :::"="::: ) "{" (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) "}" ))) ; theorem :: WAYBEL32:24 (Bool "for" (Set (Var "R")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_waybel_2 :::"sup"::: ) (Set "(" ($#k2_waybel32 :::"inf_net"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))))) ; theorem :: WAYBEL32:25 (Bool "for" (Set (Var "R")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set ($#k1_waybel_2 :::"sup"::: ) (Set "(" ($#k2_waybel32 :::"inf_net"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "N")) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i")) ")" )))))) ; theorem :: WAYBEL32:26 (Bool "for" (Set (Var "R")) "being" ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "V")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_waybel32 :::"inf_net"::: ) (Set (Var "N"))) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "V")))))) ; theorem :: WAYBEL32:27 (Bool "for" (Set (Var "R")) "being" ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "V")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "V")))) "holds" (Bool (Set ($#k2_waybel32 :::"inf_net"::: ) (Set (Var "N"))) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "V")))))) ; theorem :: WAYBEL32:28 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#v2_waybel32 :::"order_consistent"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))))) "holds" (Bool (Set (Var "x")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))))) ; theorem :: WAYBEL32:29 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#v2_waybel32 :::"order_consistent"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "N")) "being" ($#v10_waybel_0 :::"eventually-directed"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))) "iff" (Bool (Set (Var "x")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N"))) ")" )))) ;