:: WAYBEL21 semantic presentation begin definitionlet "S", "T" be ($#l1_orders_2 :::"Semilattice":::); assume "(" (Bool (Bool (Set (Const "S")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) )) "implies" (Bool (Set (Const "T")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) ")" ; mode :::"SemilatticeHomomorphism"::: "of" "S" "," "T" -> ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" means :: WAYBEL21:def 1 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "S" "holds" (Bool it ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))); end; :: deftheorem defines :::"SemilatticeHomomorphism"::: WAYBEL21:def 1 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"Semilattice":::) "st" (Bool "(" (Bool (Bool (Set (Var "S")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) )) "implies" (Bool (Set (Var "T")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) ")" ) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_waybel21 :::"SemilatticeHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))) "iff" (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "b3")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))) ")" ))); registrationlet "S", "T" be ($#l1_orders_2 :::"Semilattice":::); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v19_waybel_0 :::"meet-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; registrationlet "S" be ($#l1_orders_2 :::"Semilattice":::); let "T" be ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::); cluster -> ($#v19_waybel_0 :::"meet-preserving"::: ) for ($#m1_waybel21 :::"SemilatticeHomomorphism"::: ) "of" "S" "," "T"; end; theorem :: WAYBEL21:1 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_waybel21 :::"SemilatticeHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "T")))))) ; theorem :: WAYBEL21:2 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v19_waybel_0 :::"meet-preserving"::: ) )) "holds" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL21:3 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "f")) "being" ($#v19_waybel_0 :::"meet-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "T"))))) "holds" (Bool (Set (Var "f")) "is" ($#m1_waybel21 :::"SemilatticeHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))))) ; theorem :: WAYBEL21:4 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v19_waybel_0 :::"meet-preserving"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) ")" )) "holds" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL21:5 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#m1_waybel21 :::"SemilatticeHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))))) ; theorem :: WAYBEL21:6 (Bool "for" (Set (Var "S1")) "," (Set (Var "T1")) "," (Set (Var "S2")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "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 ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" ))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "T1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S2")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_funct_2 :::"="::: ) (Set (Var "f2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f1")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) )) "implies" (Bool (Set (Var "f2")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f1")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "implies" (Bool (Set (Var "f2")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ")" )))) ; theorem :: WAYBEL21:7 (Bool "for" (Set (Var "S1")) "," (Set (Var "T1")) "," (Set (Var "S2")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "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 ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" ))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "T1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S2")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_funct_2 :::"="::: ) (Set (Var "f2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f1")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) )) "implies" (Bool (Set (Var "f2")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f1")) "is" ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) )) "implies" (Bool (Set (Var "f2")) "is" ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) ) ")" ")" )))) ; theorem :: WAYBEL21:8 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v7_yellow_0 :::"infs-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_9 :::"incl"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ))) ; theorem :: WAYBEL21:9 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v8_yellow_0 :::"sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_9 :::"incl"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ))) ; theorem :: WAYBEL21:10 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_9 :::"incl"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ))) ; theorem :: WAYBEL21:11 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_9 :::"incl"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is" ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) ))) ; theorem :: WAYBEL21:12 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T1")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" )) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T2"))) & "(" (Bool (Bool (Set (Var "S")) "is" ($#v4_yellow_0 :::"full"::: ) )) "implies" (Bool (Set (Var "R")) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T2"))) ")" ")" ))) ; theorem :: WAYBEL21:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set (Var "T")) "is" ($#v4_yellow_0 :::"full"::: ) ($#v7_yellow_0 :::"infs-inheriting"::: ) ($#v8_yellow_0 :::"sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")))) ; registrationlet "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) ($#v7_yellow_0 :::"infs-inheriting"::: ) ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "T"; end; theorem :: WAYBEL21:14 (Bool "for" (Set (Var "T")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))) ; theorem :: WAYBEL21:15 (Bool "for" (Set (Var "T")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_yellow_0 :::"join-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))) ; theorem :: WAYBEL21:16 (Bool "for" (Set (Var "T")) "being" ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "S")) "is" ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ))) ; theorem :: WAYBEL21:17 (Bool "for" (Set (Var "T")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "S")) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ))) ; theorem :: WAYBEL21:18 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) ))) ; theorem :: WAYBEL21:19 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) ))) ; theorem :: WAYBEL21:20 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T1")) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T2")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" )) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Var "S1")) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) )) "holds" (Bool (Set (Var "S2")) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) )))) ; theorem :: WAYBEL21:21 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T1")) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T2")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" )) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Var "S1")) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) )) "holds" (Bool (Set (Var "S2")) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) )))) ; theorem :: WAYBEL21:22 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T1")) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T2")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" )) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Var "S1")) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) )) "holds" (Bool (Set (Var "S2")) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) )))) ; theorem :: WAYBEL21:23 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T1")) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T2")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" )) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Var "S1")) "is" ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) )) "holds" (Bool (Set (Var "S2")) "is" ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) )))) ; begin theorem :: WAYBEL21:24 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) (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 (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" )))))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "T")); redefine attr "N" is :::"antitone"::: means :: WAYBEL21:def 2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::">="::: ) (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))))); end; :: deftheorem defines :::"antitone"::: WAYBEL21:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v9_waybel_0 :::"antitone"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::">="::: ) (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))))) ")" ))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); cluster (Set (Set ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) ) ($#k3_yellow_9 :::"opp+id"::: ) ) -> ($#v4_orders_2 :::"transitive"::: ) ($#v7_waybel_0 :::"directed"::: ) ($#v8_waybel_0 :::"monotone"::: ) ($#v9_waybel_0 :::"antitone"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ($#v8_waybel_0 :::"monotone"::: ) ($#v9_waybel_0 :::"antitone"::: ) for ($#l1_waybel_0 :::"NetStr"::: ) "over" "T"; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "F" ($#k3_yellow_9 :::"opp+id"::: ) ) -> ($#v9_waybel_0 :::"antitone"::: ) ; end; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; 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"::: ) ) ($#v9_waybel_0 :::"antitone"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); cluster (Set "f" ($#k6_waybel_9 :::"*"::: ) "N") -> ($#v9_waybel_0 :::"antitone"::: ) ; end; theorem :: WAYBEL21:25 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "holds" (Bool "{" (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 "S")) ")" ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool verum) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))))) ; theorem :: WAYBEL21:26 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "N")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v8_waybel_0 :::"monotone"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "holds" (Bool "{" (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 "S")) ")" ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool verum) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))))) ; theorem :: WAYBEL21:27 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL21:28 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "F")) ($#k3_yellow_9 :::"opp+id"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "F")))))) ; theorem :: WAYBEL21:29 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#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 "(" (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" )))))) ; theorem :: WAYBEL21:30 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopPoset":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set "(" (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ")" )) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Set (Var "Y")) ($#k3_yellow_9 :::"opp+id"::: ) )))))) ; theorem :: WAYBEL21:31 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopPoset":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k10_yellow_6 :::"Lim"::: ) (Set "(" (Set (Var "Y")) ($#k3_yellow_9 :::"opp+id"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set "(" (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ")" ) ")" ))))))) ; theorem :: WAYBEL21:32 (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 "(" (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "D")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D"))) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "S"))) ")" ))) ; theorem :: WAYBEL21:33 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (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 "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "D")) ")" )))))) ; theorem :: WAYBEL21:34 (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"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" ) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r3_orders_2 :::"<="::: ) (Set (Var "j"))) "iff" (Bool (Set (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))) ")" )))) ; theorem :: WAYBEL21:35 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" ))))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "T")); let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "T")); assume (Bool (Set (Const "M")) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Const "N"))) ; mode :::"Embedding"::: "of" "M" "," "N" -> ($#m1_subset_1 :::"Function":::) "of" "M" "," "N" means :: WAYBEL21:def 3 (Bool "(" (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "M") ($#r2_relset_1 :::"="::: ) (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N") ($#k1_partfun1 :::"*"::: ) it)) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "n")) ($#r1_orders_2 :::"<="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "m")) ($#r1_orders_2 :::"<="::: ) (Set it ($#k2_yellow_6 :::"."::: ) (Set (Var "p")))))) ")" ) ")" ); end; :: deftheorem defines :::"Embedding"::: WAYBEL21:def 3 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "T")) "st" (Bool (Bool (Set (Var "M")) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_waybel21 :::"Embedding"::: ) "of" (Set (Var "M")) "," (Set (Var "N"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "M"))) ($#r2_relset_1 :::"="::: ) (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))) ($#k1_partfun1 :::"*"::: ) (Set (Var "b4")))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "n")) ($#r1_orders_2 :::"<="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "m")) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "b4")) ($#k2_yellow_6 :::"."::: ) (Set (Var "p")))))) ")" ) ")" ) ")" ))))); theorem :: WAYBEL21:36 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "e")) "being" ($#m2_waybel21 :::"Embedding"::: ) "of" (Set (Var "M")) "," (Set (Var "N")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "M")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set "(" (Set (Var "e")) ($#k2_yellow_6 :::"."::: ) (Set (Var "i")) ")" )))))))) ; theorem :: WAYBEL21:37 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M"))))))) ; theorem :: WAYBEL21:38 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "e")) "being" ($#m2_waybel21 :::"Embedding"::: ) "of" (Set (Var "M")) "," (Set (Var "N")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "e")) ($#k2_yellow_6 :::"."::: ) (Set (Var "j"))) ($#r1_orders_2 :::"<="::: ) (Set (Var "i")))) "holds" (Bool "ex" (Set (Var "j9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "j9")) ($#r1_orders_2 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::">="::: ) (Set (Set (Var "M")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j9")))) ")" ))) ")" )) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M")))))))) ; theorem :: WAYBEL21:39 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_6 :::"full"::: ) ($#m1_yellow_6 :::"SubNetStr"::: ) "of" (Set (Var "N")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set (Var "j")) ($#r1_orders_2 :::">="::: ) (Set (Var "i"))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N"))) & (Bool (Set ($#k1_yellow_9 :::"incl"::: ) "(" (Set (Var "M")) "," (Set (Var "N")) ")" ) "is" ($#m2_waybel21 :::"Embedding"::: ) "of" (Set (Var "M")) "," (Set (Var "N"))) ")" )))) ; theorem :: WAYBEL21:40 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Set (Var "N")) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i"))) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N"))) & (Bool (Set ($#k1_yellow_9 :::"incl"::: ) "(" (Set "(" (Set (Var "N")) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ) "," (Set (Var "N")) ")" ) "is" ($#m2_waybel21 :::"Embedding"::: ) "of" (Set (Set (Var "N")) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i"))) "," (Set (Var "N"))) ")" )))) ; theorem :: WAYBEL21:41 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "N")) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))))))) ; theorem :: WAYBEL21:42 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set "(" (Set (Var "N")) ($#k5_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))))) ; theorem :: WAYBEL21:43 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "N")) "being" ($#v11_waybel_0 :::"eventually-filtered"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))))) ; theorem :: WAYBEL21:44 (Bool "for" (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "N")) "being" ($#v11_waybel_0 :::"eventually-filtered"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_waybel_9 :::"inf"::: ) (Set (Var "N")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; begin theorem :: WAYBEL21:45 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#v19_waybel_0 :::"meet-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) ")" ) ")" ) ")" ))) ; theorem :: WAYBEL21:46 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_waybel21 :::"SemilatticeHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ) ")" ))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"lim_infs-preserving"::: means :: WAYBEL21:def 4 (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" "S" "holds" (Bool (Set "f" ($#k2_yellow_6 :::"."::: ) (Set "(" ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" "f" ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" )))); end; :: deftheorem defines :::"lim_infs-preserving"::: WAYBEL21:def 4 : (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_waybel21 :::"lim_infs-preserving"::: ) ) "iff" (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set "(" ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" )))) ")" ))); theorem :: WAYBEL21:47 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_waybel21 :::"SemilatticeHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v1_waybel21 :::"lim_infs-preserving"::: ) ) ")" ))) ; theorem :: WAYBEL21:48 (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "X")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) "holds" (Bool (Set (Var "S")) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ))) ; theorem :: WAYBEL21:49 (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "X")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) "holds" (Bool (Set (Var "S")) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ))) ; theorem :: WAYBEL21:50 (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v7_yellow_0 :::"infs-inheriting"::: ) ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "X")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; theorem :: WAYBEL21:51 (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v7_yellow_0 :::"infs-inheriting"::: ) ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))))) ; theorem :: WAYBEL21:52 (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool "(" "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ))) ; theorem :: WAYBEL21:53 (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ))) ; theorem :: WAYBEL21:54 (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel19 :::"Lawson"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )))) ;