:: WAYBEL33 semantic presentation begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Const "X")) ")" ); func :::"lim_inf"::: "F" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: WAYBEL33:def 1 (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "B")) ")" ) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "L" : (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "F") "}" "," "L" ")" ); end; :: deftheorem defines :::"lim_inf"::: WAYBEL33:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "B")) ")" ) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) : (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" "," (Set (Var "L")) ")" ))))); theorem :: WAYBEL33:1 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "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 "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2")) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X1")) ")" ) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X2")) ")" ) "st" (Bool (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Var "F2")))) "holds" (Bool (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F2"))))))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) ; attr "L" is :::"lim-inf"::: means :: WAYBEL33:def 2 (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "L") ($#r1_hidden :::"="::: ) (Set ($#k4_waybel28 :::"xi"::: ) "L")); end; :: deftheorem defines :::"lim-inf"::: WAYBEL33:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_waybel33 :::"lim-inf"::: ) ) "iff" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L")))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_waybel33 :::"lim-inf"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) 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"::: ) -> ($#v1_waybel33 :::"lim-inf"::: ) 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"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v1_waybel33 :::"lim-inf"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; theorem :: WAYBEL33:2 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))))) "holds" (Bool "for" (Set (Var "N1")) "being" ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L1")) (Bool "ex" (Set (Var "N2")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L2")) "st" (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N2"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N1"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N2")))) ")" )))) ; theorem :: WAYBEL33:3 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))))) "holds" (Bool "for" (Set (Var "N1")) "being" ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L1")) "st" (Bool (Bool (Set (Var "N1")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L1"))))) "holds" (Bool "ex" (Set (Var "N2")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L2")) "st" (Bool "(" (Bool (Set (Var "N2")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L2")))) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N2"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N1"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N2")))) ")" )))) ; theorem :: WAYBEL33:4 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "N1")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "N2")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N2"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N1"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N2"))))) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N2"))))))) ; theorem :: WAYBEL33:5 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))))) "holds" (Bool "for" (Set (Var "N1")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "N2")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N2"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N1"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N2"))))) "holds" (Bool "for" (Set (Var "S1")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N1")) (Bool "ex" (Set (Var "S2")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N2")) "st" (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S2"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "S1"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "S2")))) ")" )))))) ; theorem :: WAYBEL33:6 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "N1")) "being" ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L1")) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N1")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L1"))))) "holds" (Bool "ex" (Set (Var "N2")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L2")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N2")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L2")))) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N2"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N1"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N2")))) ")" ))))) ; theorem :: WAYBEL33:7 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L1")) (Bool "for" (Set (Var "N2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L2")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N2"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N1"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N2"))))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "N1")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "N2")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X"))))))) ; theorem :: WAYBEL33:8 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool (Set ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L2")) ")" )))) ; theorem :: WAYBEL33:9 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L2"))))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v25_waybel_0 :::"/\-complete"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; registrationlet "R" be ($#l1_orders_2 :::"Semilattice":::); cluster -> ($#v2_lattice3 :::"with_infima"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; registrationlet "L" be ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v1_waybel33 :::"lim-inf"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "L"; end; theorem :: WAYBEL33:10 (Bool "for" (Set (Var "L")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "X")) "being" ($#v1_waybel33 :::"lim-inf"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))))) ; definitionlet "L" be ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::); func :::"Xi"::: "L" -> ($#v1_waybel_9 :::"strict"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "L" means :: WAYBEL33:def 3 (Bool it "is" ($#v1_waybel33 :::"lim-inf"::: ) ); end; :: deftheorem defines :::"Xi"::: WAYBEL33:def 3 : (Bool "for" (Set (Var "L")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_waybel_9 :::"strict"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel33 :::"Xi"::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "b2")) "is" ($#v1_waybel33 :::"lim-inf"::: ) ) ")" ))); registrationlet "L" be ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Semilattice":::); cluster (Set ($#k2_waybel33 :::"Xi"::: ) "L") -> ($#v1_waybel_9 :::"strict"::: ) ($#v1_waybel33 :::"lim-inf"::: ) ; end; theorem :: WAYBEL33:11 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k1_waybel_9 :::"inf"::: ) (Set "(" (Set (Var "N")) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ) ")" ) where i "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool verum) "}" "," (Set (Var "L")) ")" )))) ; theorem :: WAYBEL33:12 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "F")) "being" ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Set (Var "i")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set "(" (Set "(" ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F")) ")" ) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ))))))) ; theorem :: WAYBEL33:13 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "F")) "being" ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F")) ")" ))))) ; theorem :: WAYBEL33:14 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "F")) "being" ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool (Set ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL33:15 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "F")) "being" ($#v3_waybel_7 :::"ultra"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "for" (Set (Var "p")) "being" ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F")) ")" ) "holds" (Bool (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F"))) ($#r1_orders_2 :::">="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set "(" (Set "(" ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F")) ")" ) ($#k2_waybel28 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: WAYBEL33:16 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "F")) "being" ($#v3_waybel_7 :::"ultra"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set ($#k3_yellow19 :::"a_net"::: ) (Set (Var "F"))) "holds" (Bool (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M"))))))) ; theorem :: WAYBEL33:17 (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" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "N")) ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "N9")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N9")))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "N9")) "is" ($#m1_yellow_6 :::"SubNetStr"::: ) "of" (Set (Var "N"))) ")" ))))) ; theorem :: WAYBEL33:18 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v1_waybel33 :::"lim-inf"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#v3_waybel_7 :::"ultra"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))) ; theorem :: WAYBEL33:19 (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_tarski :::"c="::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L"))))) ; theorem :: WAYBEL33:20 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2"))))) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2")))))) ; theorem :: WAYBEL33:21 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k1_waybel19 :::"omega"::: ) (Set (Var "L"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L"))))) ; theorem :: WAYBEL33:22 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T1"))) & (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T2")))) "holds" (Bool "for" (Set (Var "R")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "R")))))) ; theorem :: WAYBEL33:23 (Bool "for" (Set (Var "T1")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T2")) "being" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T1")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "implies" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))) ")" & "(" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "implies" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))) ")" ")" )))) ; theorem :: WAYBEL33:24 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k2_waybel19 :::"lambda"::: ) (Set (Var "L"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L"))))) ; theorem :: WAYBEL33:25 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v1_waybel33 :::"lim-inf"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "S")) "being" ($#v2_pre_topc :::"correct"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) "holds" (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "S")))))) ; theorem :: WAYBEL33:26 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v1_waybel33 :::"lim-inf"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "F")) "being" ($#v3_waybel_7 :::"ultra"::: ) ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool (Set ($#k1_waybel33 :::"lim_inf"::: ) (Set (Var "F"))) ($#r2_waybel_7 :::"is_a_convergence_point_of"::: ) (Set (Var "F")) "," (Set (Var "L"))))) ; theorem :: WAYBEL33:27 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v1_waybel33 :::"lim-inf"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "L")) "is" ($#v7_pre_topc :::"T_1"::: ) ) ")" )) ;