:: WAYBEL17 semantic presentation begin definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); func "(" "a" "," "b" ")" :::",..."::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "S" means :: WAYBEL17:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")))))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "a") ")" & "(" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k"))))) ")" )) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "b") ")" ")" )); end; :: deftheorem defines :::",..."::: WAYBEL17:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k1_waybel17 :::",..."::: ) )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")))))) "implies" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k"))))) ")" )) "implies" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ")" )) ")" )))); scheme :: WAYBEL17:sch 1 FuncFraenkelS{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ), F4() -> ($#m1_hidden :::"Function":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set (Set F4 "(" ")" ) ($#k7_relat_1 :::".:"::: ) "{" (Set F3 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F3 "(" (Set (Var "x")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ) provided (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F4 "(" ")" ))) proof end; scheme :: WAYBEL17:sch 2 FuncFraenkelSL{ F1() -> ($#l1_orders_2 :::"LATTICE":::), F2() -> ($#l1_orders_2 :::"LATTICE":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ), F4() -> ($#m1_hidden :::"Function":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set (Set F4 "(" ")" ) ($#k7_relat_1 :::".:"::: ) "{" (Set F3 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F3 "(" (Set (Var "x")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ) provided (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F4 "(" ")" ))) proof end; theorem :: WAYBEL17:1 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))) "is" ($#v12_waybel_0 :::"lower"::: ) )))) ; theorem :: WAYBEL17:2 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))) "is" ($#v13_waybel_0 :::"upper"::: ) )))) ; theorem :: WAYBEL17:3 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v22_waybel_0 :::"directed-sups-preserving"::: ) -> ($#v5_orders_3 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))))); end; theorem :: WAYBEL17:4 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; registrationlet "S", "T" be ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v5_pre_topc :::"continuous"::: ) -> ($#v5_orders_3 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))))); end; begin registrationlet "S" be ($#m1_hidden :::"set"::: ) ; let "T" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "S" ($#k2_funcop_1 :::"-->"::: ) "T") -> ($#v5_waybel_3 :::"reflexive-yielding"::: ) ; end; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set "T" ($#k6_yellow_1 :::"|^"::: ) "S") -> ($#v3_lattice3 :::"complete"::: ) ; end; definitionlet "S", "T" be ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::); func :::"SCMaps"::: "(" "S" "," "T" ")" -> ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set ($#k7_yellow_1 :::"MonMaps"::: ) "(" "S" "," "T" ")" ) means :: WAYBEL17:def 2 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "iff" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )); end; :: deftheorem defines :::"SCMaps"::: WAYBEL17:def 2 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "b3")) "being" ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set ($#k7_yellow_1 :::"MonMaps"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel17 :::"SCMaps"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" )) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3")))) "iff" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) ")" ))); registrationlet "S", "T" be ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster (Set ($#k2_waybel17 :::"SCMaps"::: ) "(" "S" "," "T" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ; end; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func :::"Net-Str"::: "(" "a" "," "b" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "S" means :: WAYBEL17:def 3 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set "(" "a" "," "b" ")" ($#k1_waybel17 :::",..."::: ) )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "for" (Set (Var "i9")) "," (Set (Var "j9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i9"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "j9")))) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j"))) "iff" (Bool (Set (Var "i9")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j9"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Net-Str"::: WAYBEL17:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "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 ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b4"))) ($#r1_funct_2 :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k1_waybel17 :::",..."::: ) )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b4")) (Bool "for" (Set (Var "i9")) "," (Set (Var "j9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i9"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "j9")))) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j"))) "iff" (Bool (Set (Var "i9")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j9"))) ")" )) ")" ) ")" ) ")" )))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k3_waybel17 :::"Net-Str"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL17:5 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "or" (Bool (Set (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))) ; theorem :: WAYBEL17:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) (Bool "for" (Set (Var "i9")) "," (Set (Var "j9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i9")) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Var "j9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i9")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j9")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "implies" (Bool (Set (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "implies" (Bool (Set (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ")" ))))) ; theorem :: WAYBEL17:7 (Bool "for" (Set (Var "S")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))))) ; theorem :: WAYBEL17:8 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set "(" ($#k3_waybel17 :::"Net-Str"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S")); func :::"Net-Str"::: "D" -> ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "S" equals :: WAYBEL17:def 4 (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" "D" "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "S") ($#k1_toler_1 :::"|_2"::: ) "D" ")" ) "," (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ")" ) ($#k1_nattra_1 :::"|"::: ) "D" ")" ) "#)" ); end; :: deftheorem defines :::"Net-Str"::: WAYBEL17:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" (Set (Var "D")) "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) ($#k1_toler_1 :::"|_2"::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_nattra_1 :::"|"::: ) (Set (Var "D")) ")" ) "#)" )))); theorem :: WAYBEL17:9 (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 "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel11 :::"Net-Str"::: ) "(" (Set (Var "D")) "," (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_nattra_1 :::"|"::: ) (Set (Var "D")) ")" ) ")" )))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S")); cluster (Set ($#k4_waybel17 :::"Net-Str"::: ) "D") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S")); cluster (Set ($#k4_waybel17 :::"Net-Str"::: ) "D") -> ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S")); cluster (Set ($#k4_waybel17 :::"Net-Str"::: ) "D") -> ($#v6_waybel_0 :::"strict"::: ) ($#v8_waybel_0 :::"monotone"::: ) ; end; theorem :: WAYBEL17:10 (Bool "for" (Set (Var "S")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (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 "S")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D")))))) ; begin theorem :: WAYBEL17:11 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" ))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; scheme :: WAYBEL17:sch 3 NetFraenkelS{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) , F3() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element":::) "of" (Set F3 "(" ")" ), F5() -> ($#m1_hidden :::"Function":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set (Set F5 "(" ")" ) ($#k7_relat_1 :::".:"::: ) "{" (Set F4 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set F4 "(" (Set (Var "x")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ) provided (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F3 "(" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F5 "(" ")" ))) and (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F1 "(" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set F2 "(" ")" ))) proof end; theorem :: WAYBEL17:12 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "w")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x"))) "}" "," (Set (Var "T")) ")" ))))) ; theorem :: WAYBEL17:13 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "w")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x"))) "}" "," (Set (Var "T")) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )))) ; theorem :: WAYBEL17:14 (Bool "for" (Set (Var "S")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "w")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x"))) "}" "," (Set (Var "T")) ")" )) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r1_waybel_3 :::"<<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_waybel_3 :::"<<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")))) ")" )) ")" )))))) ; theorem :: WAYBEL17:15 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D")) "," (Set (Var "S"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D"))) "," (Set (Var "T"))) ")" ) "or" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "S")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool (Set (Var "T")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "T")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) ")" ) ")" ) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D")) ")" )) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D")) ")" )))))) ; theorem :: WAYBEL17:16 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "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 "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D")) "," (Set (Var "S"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D"))) "," (Set (Var "T"))) ")" ) "or" (Bool "(" (Bool (Set (Var "S")) "is" ($#v24_waybel_0 :::"up-complete"::: ) ) & (Bool (Set (Var "T")) "is" ($#v24_waybel_0 :::"up-complete"::: ) ) ")" ) ")" ) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D")) ")" )))))) ; theorem :: WAYBEL17:17 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D")) "," (Set (Var "S"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D"))) "," (Set (Var "T"))) ")" ) "or" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "S")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool (Set (Var "T")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "T")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) ")" ) ")" ) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "D")) ")" )) ($#r1_orders_2 :::"<="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D")) ")" )))))) ; theorem :: WAYBEL17:18 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_waybel_0 :::"monotone"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N"))) "is" ($#v8_waybel_0 :::"monotone"::: ) )))) ; registrationlet "S", "T" be ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"LATTICE":::); let "f" be ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_waybel_0 :::"monotone"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); cluster (Set "f" ($#k6_waybel_9 :::"*"::: ) "N") -> ($#v8_waybel_0 :::"monotone"::: ) ; end; theorem :: WAYBEL17:19 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" ))) ")" )) "holds" (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 "S")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D")) ")" )))))) ; theorem :: WAYBEL17:20 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "j9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" ) "st" (Bool (Bool (Set (Var "j9")) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (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 "j"))) "}" "," (Set (Var "S")) ")" ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "l")) ")" ) where l "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" ) : (Bool (Set (Var "l")) ($#r1_orders_2 :::">="::: ) (Set (Var "j9"))) "}" "," (Set (Var "T")) ")" ))))))) ; begin theorem :: WAYBEL17:21 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" )))) ")" ))) ; theorem :: WAYBEL17:22 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ))) ; registrationlet "S", "T" be ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v5_pre_topc :::"continuous"::: ) -> ($#v22_waybel_0 :::"directed-sups-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))))); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v22_waybel_0 :::"directed-sups-preserving"::: ) -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))))); end; theorem :: WAYBEL17:23 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r1_waybel_3 :::"<<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_waybel_3 :::"<<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")))) ")" )) ")" ))) ")" ))) ; theorem :: WAYBEL17:24 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "w")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x"))) "}" "," (Set (Var "T")) ")" ))) ")" ))) ; theorem :: WAYBEL17:25 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool "(" (Bool (Set (Var "w")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "w")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ) "}" "," (Set (Var "T")) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )))) ; theorem :: WAYBEL17:26 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool "(" (Bool (Set (Var "w")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "w")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ) "}" "," (Set (Var "T")) ")" )) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "w")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x"))) "}" "," (Set (Var "T")) ")" ))))) ; theorem :: WAYBEL17:27 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) & (Bool (Set (Var "T")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "T")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "j")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "k")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")))) ")" )) ")" ))) ")" ))) ; theorem :: WAYBEL17:28 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) & (Bool (Set (Var "T")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool "(" (Bool (Set (Var "w")) ($#r3_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "w")) "is" ($#v1_waybel_3 :::"compact"::: ) ) ")" ) "}" "," (Set (Var "T")) ")" ))) ")" ))) ; theorem :: WAYBEL17:29 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~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"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ;