:: WAYBEL34 semantic presentation begin registrationlet "S", "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster ($#v3_waybel_1 :::"Galois"::: ) for ($#m1_waybel_1 :::"Connection"::: ) "of" "S" "," "T"; end; theorem :: WAYBEL34:1 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "S9")) "," (Set (Var "T9")) "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 "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 "S9"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S9"))) "#)" )) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T9"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T9"))) "#)" ))) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "c9")) "being" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S9")) "," (Set (Var "T9")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9"))) & (Bool (Set (Var "c")) "is" ($#v3_waybel_1 :::"Galois"::: ) )) "holds" (Bool (Set (Var "c9")) "is" ($#v3_waybel_1 :::"Galois"::: ) )))) ; definitionlet "S", "T" be ($#l1_orders_2 :::"LATTICE":::); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); assume that (Bool (Set (Const "S")) "is" ($#v3_lattice3 :::"complete"::: ) ) and (Bool (Set (Const "g")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) ; func :::"LowerAdj"::: "g" -> ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" means :: WAYBEL34:def 1 (Bool (Set ($#k1_waybel_1 :::"["::: ) "g" "," it ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ); end; :: deftheorem defines :::"LowerAdj"::: WAYBEL34:def 1 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "g")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")))) "iff" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "b4")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) ")" )))); definitionlet "S", "T" be ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); assume that (Bool (Set (Const "T")) "is" ($#v3_lattice3 :::"complete"::: ) ) and (Bool (Set (Const "d")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) ; func :::"UpperAdj"::: "d" -> ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" means :: WAYBEL34:def 2 (Bool (Set ($#k1_waybel_1 :::"["::: ) it "," "d" ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ); end; :: deftheorem defines :::"UpperAdj"::: WAYBEL34:def 2 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "d")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "d")))) "iff" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "b4")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) ")" )))); registrationlet "S", "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); let "g" be ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); cluster (Set ($#k1_waybel34 :::"LowerAdj"::: ) "g") -> ($#v5_waybel_1 :::"lower_adjoint"::: ) ; end; registrationlet "S", "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); cluster (Set ($#k2_waybel34 :::"UpperAdj"::: ) "d") -> ($#v4_waybel_1 :::"upper_adjoint"::: ) ; end; theorem :: WAYBEL34:2 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "t")) ")" ) ")" )))))) ; theorem :: WAYBEL34:3 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "d")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "d")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "s")) ")" ) ")" )))))) ; definitionlet "S", "T" be ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "T"))); func "f" :::"opp"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "S" ($#k7_lattice3 :::"opp"::: ) ")" ) "," (Set "(" "T" ($#k7_lattice3 :::"opp"::: ) ")" ) equals :: WAYBEL34:def 3 "f"; end; :: deftheorem defines :::"opp"::: WAYBEL34:def 3 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "holds" (Bool (Set (Set (Var "f")) ($#k3_waybel34 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))); registrationlet "S", "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); let "g" be ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); cluster (Set "g" ($#k3_waybel34 :::"opp"::: ) ) -> ($#v5_waybel_1 :::"lower_adjoint"::: ) ; end; registrationlet "S", "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); cluster (Set "d" ($#k3_waybel34 :::"opp"::: ) ) -> ($#v4_waybel_1 :::"upper_adjoint"::: ) ; end; theorem :: WAYBEL34:4 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g"))) ($#r1_funct_2 :::"="::: ) (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" (Set (Var "g")) ($#k3_waybel34 :::"opp"::: ) ")" ))))) ; theorem :: WAYBEL34:5 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" (Set (Var "d")) ($#k3_waybel34 :::"opp"::: ) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "d")))))) ; theorem :: WAYBEL34:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "L")) ")" ) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )) ; theorem :: WAYBEL34:7 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L")))) & (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L")))) ")" )) ; theorem :: WAYBEL34:8 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g1")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) (Bool "for" (Set (Var "g2")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L2")) "," (Set (Var "L3")) "holds" (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" (Set (Var "g2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g1")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g1")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g2")) ")" )))))) ; theorem :: WAYBEL34:9 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d1")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) (Bool "for" (Set (Var "d2")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L2")) "," (Set (Var "L3")) "holds" (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" (Set (Var "d2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d1")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "d1")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "d2")) ")" )))))) ; theorem :: WAYBEL34:10 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))) ; theorem :: WAYBEL34:11 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "d")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "d"))))) ; theorem :: WAYBEL34:12 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool "ex" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2"))) ")" )))) ; definitionlet "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; given "w" being ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "W")) such that (Bool (Bool "not" (Set (Const "w")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; func "W" :::"-INF_category"::: -> ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) means :: WAYBEL34:def 4 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" it) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "x")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) "W") ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" it (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"-INF_category"::: WAYBEL34:def 4 : (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "not" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Var "w")) "is" ($#v1_xboole_0 :::"empty"::: ) )))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "x")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) ")" )) ")" ) ")" ) ")" ))); definitionlet "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; given "w" being ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "W")) such that (Bool (Bool "not" (Set (Const "w")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; func "W" :::"-SUP_category"::: -> ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) means :: WAYBEL34:def 5 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" it) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "x")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) "W") ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" it (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"-SUP_category"::: WAYBEL34:def 5 : (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "not" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Var "w")) "is" ($#v1_xboole_0 :::"empty"::: ) )))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#l2_altcat_1 :::"category":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "x")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2")) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k3_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) ")" )) ")" ) ")" ) ")" ))); registrationlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "W" ($#k4_waybel34 :::"-INF_category"::: ) ) -> ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#v3_yellow21 :::"with_complete_lattices"::: ) ; cluster (Set "W" ($#k5_waybel34 :::"-SUP_category"::: ) ) -> ($#v6_altcat_1 :::"strict"::: ) ($#v2_yellow21 :::"lattice-wise"::: ) ($#v3_yellow21 :::"with_complete_lattices"::: ) ; end; theorem :: WAYBEL34:13 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ))) ; theorem :: WAYBEL34:14 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" )) ")" )))) ; theorem :: WAYBEL34:15 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ))) ; theorem :: WAYBEL34:16 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" )) ")" )))) ; theorem :: WAYBEL34:17 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" )))) ; definitionlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; func "W" :::"LowerAdj"::: -> ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set "W" ($#k4_waybel34 :::"-INF_category"::: ) ) "," (Set "W" ($#k5_waybel34 :::"-SUP_category"::: ) ) means :: WAYBEL34:def 6 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k4_waybel34 :::"-INF_category"::: ) ")" ) "holds" (Bool (Set it ($#k3_functor0 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k4_waybel34 :::"-INF_category"::: ) ")" ) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set it ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" )))) ")" ) ")" ); func "W" :::"UpperAdj"::: -> ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set "W" ($#k5_waybel34 :::"-SUP_category"::: ) ) "," (Set "W" ($#k4_waybel34 :::"-INF_category"::: ) ) means :: WAYBEL34:def 7 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) "holds" (Bool (Set it ($#k3_functor0 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set it ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"LowerAdj"::: WAYBEL34:def 6 : (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ) "," (Set (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k6_waybel34 :::"LowerAdj"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" ) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "b2")) ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" )))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"UpperAdj"::: WAYBEL34:def 7 : (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ) "," (Set (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k7_waybel34 :::"UpperAdj"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_functor0 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "b2")) ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" )))) ")" ) ")" ) ")" ))); registrationlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "W" ($#k6_waybel34 :::"LowerAdj"::: ) ) -> ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#v21_functor0 :::"bijective"::: ) ; cluster (Set "W" ($#k7_waybel34 :::"UpperAdj"::: ) ) -> ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#v21_functor0 :::"bijective"::: ) ; end; theorem :: WAYBEL34:18 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k6_waybel34 :::"LowerAdj"::: ) ")" ) ($#k15_functor0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k7_waybel34 :::"UpperAdj"::: ) )) & (Bool (Set (Set "(" (Set (Var "W")) ($#k7_waybel34 :::"UpperAdj"::: ) ")" ) ($#k15_functor0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k6_waybel34 :::"LowerAdj"::: ) )) ")" )) ; theorem :: WAYBEL34:19 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k6_waybel34 :::"LowerAdj"::: ) ")" ) ($#k13_functor0 :::"*"::: ) (Set "(" (Set (Var "W")) ($#k7_waybel34 :::"UpperAdj"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_functor0 :::"id"::: ) (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" ))) & (Bool (Set (Set "(" (Set (Var "W")) ($#k7_waybel34 :::"UpperAdj"::: ) ")" ) ($#k13_functor0 :::"*"::: ) (Set "(" (Set (Var "W")) ($#k6_waybel34 :::"LowerAdj"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_functor0 :::"id"::: ) (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" ))) ")" )) ; theorem :: WAYBEL34:20 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ) "," (Set (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ) ($#r2_functor0 :::"are_anti-isomorphic"::: ) )) ; begin theorem :: WAYBEL34:21 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "V")) ")" )) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")))))) ")" ))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"waybelow-preserving"::: means :: WAYBEL34:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y")))) "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_waybel_3 :::"<<"::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"waybelow-preserving"::: WAYBEL34:def 8 : (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")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_waybel34 :::"waybelow-preserving"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_waybel_3 :::"<<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ))); theorem :: WAYBEL34:22 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g"))) "is" ($#v1_waybel34 :::"waybelow-preserving"::: ) ))) ; theorem :: WAYBEL34:23 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g"))) "is" ($#v1_waybel34 :::"waybelow-preserving"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )))) ; definitionlet "S", "T" be ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"relatively_open"::: means :: WAYBEL34:def 9 (Bool "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" "S" "holds" (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) (Set (Var "V"))) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "T" ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "f" ")" ) ")" ))); end; :: deftheorem defines :::"relatively_open"::: WAYBEL34:def 9 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_waybel34 :::"relatively_open"::: ) ) "iff" (Bool "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "V"))) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ))) ")" ))); theorem :: WAYBEL34:24 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#v2_waybel34 :::"relatively_open"::: ) ) "iff" (Bool (Set ($#k8_waybel18 :::"corestr"::: ) (Set (Var "d"))) "is" ($#v1_t_0topsp :::"open"::: ) ) ")" ))) ; theorem :: WAYBEL34:25 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "V")) ")" ) ")" )))))))) ; theorem :: WAYBEL34:26 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "V")) ")" )) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y"))) ")" )) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "d")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "d")) "is" ($#v2_waybel34 :::"relatively_open"::: ) )))))) ; registrationlet "X", "Y" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); let "f" be ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set ($#k1_yellow_2 :::"Image"::: ) "f") -> ($#v3_lattice3 :::"complete"::: ) ; end; theorem :: WAYBEL34:27 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "Z")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k1_yellow_2 :::"Image"::: ) (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" )) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "d")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")))) & (Bool (Set (Var "d9")) ($#r1_funct_2 :::"="::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) "is" ($#v2_waybel34 :::"relatively_open"::: ) )) "holds" (Bool (Set (Var "d9")) "is" ($#v1_t_0topsp :::"open"::: ) )))))))) ; theorem :: WAYBEL34:28 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "g")) "is" bbbadV2_FUNCT_1())) "holds" (Bool "for" (Set (Var "X")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "d")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) "iff" (Bool (Set (Var "d")) "is" ($#v1_t_0topsp :::"open"::: ) ) ")" )))))) ; registrationlet "X" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); let "f" be ($#v6_waybel_1 :::"projection"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set ($#k1_yellow_2 :::"Image"::: ) "f") -> ($#v3_lattice3 :::"complete"::: ) ; end; theorem :: WAYBEL34:29 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "k")) "being" ($#v8_waybel_1 :::"kernel"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "k"))) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "k"))) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) & (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "k")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "k")))) & (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "k")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "k")))) ")" ))) ; theorem :: WAYBEL34:30 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "k")) "being" ($#v8_waybel_1 :::"kernel"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "k")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) "iff" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "k"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ))) ; theorem :: WAYBEL34:31 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "k")) "being" ($#v8_waybel_1 :::"kernel"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "k")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "k"))) (Bool "for" (Set (Var "Y")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")))) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "V"))) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")))))) ")" ))) ; theorem :: WAYBEL34:32 (Bool "for" (Set (Var "L")) "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 "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "a")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "b"))))))) ; theorem :: WAYBEL34:33 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "k")) "being" ($#v8_waybel_1 :::"kernel"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "k")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "k")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "a")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "b"))) ")" ))))) ; theorem :: WAYBEL34:34 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "k")) "being" ($#v8_waybel_1 :::"kernel"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "k"))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "k")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "a")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "b"))) ")" )) ")" )) "holds" (Bool (Set (Var "k")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ))) ; theorem :: WAYBEL34:35 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "c"))) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) & (Bool (Set ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "c"))) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "c")))) & (Bool (Set ($#k1_waybel34 :::"LowerAdj"::: ) (Set "(" ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "c")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "c")))) ")" ))) ; theorem :: WAYBEL34:36 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c"))) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ) "iff" (Bool (Set ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "c"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ))) ; theorem :: WAYBEL34:37 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c"))) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c"))) (Bool "for" (Set (Var "Y")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "f")) "is" ($#v1_t_0topsp :::"open"::: ) )))) ")" ))) ; theorem :: WAYBEL34:38 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c"))) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) )) "holds" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "c"))) "is" ($#v1_waybel34 :::"waybelow-preserving"::: ) ))) ; theorem :: WAYBEL34:39 (Bool "for" (Set (Var "L")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "c")) "being" ($#v7_waybel_1 :::"closure"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "c"))) "is" ($#v1_waybel34 :::"waybelow-preserving"::: ) )) "holds" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c"))) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ))) ; begin definitionlet "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func "W" :::"-INF(SC)_category"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set "W" ($#k4_waybel34 :::"-INF_category"::: ) ) means :: WAYBEL34:def 10 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k4_waybel34 :::"-INF_category"::: ) ")" ) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" it) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k4_waybel34 :::"-INF_category"::: ) ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"object":::) "of" it "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a9")) "," (Set (Var "b9")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set ($#k5_yellow21 :::"@"::: ) (Set (Var "f"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-INF(SC)_category"::: WAYBEL34:def 10 : (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" ) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2")) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a9")) "," (Set (Var "b9")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set ($#k5_yellow21 :::"@"::: ) (Set (Var "f"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ))) ")" ) ")" ) ")" ))); definitionlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; func "W" :::"-SUP(SO)_category"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set "W" ($#k5_waybel34 :::"-SUP_category"::: ) ) means :: WAYBEL34:def 11 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" it) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"object":::) "of" it "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a9")) "," (Set (Var "b9")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" )) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-SUP(SO)_category"::: WAYBEL34:def 11 : (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_waybel34 :::"-SUP(SO)_category"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k5_waybel34 :::"-SUP_category"::: ) ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2")) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a9")) "," (Set (Var "b9")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set "(" ($#k5_yellow21 :::"@"::: ) (Set (Var "f")) ")" )) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" ))) ")" ) ")" ) ")" ))); theorem :: WAYBEL34:40 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (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 "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Set (Var "S")) ($#k6_struct_0 :::"-->"::: ) (Set (Var "t"))) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "S")) ($#k6_struct_0 :::"-->"::: ) (Set (Var "t"))) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) ")" ))))) ; theorem :: WAYBEL34:41 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set (Set (Var "S")) ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "T")) ")" )) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ))) ; theorem :: WAYBEL34:42 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set (Set (Var "S")) ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "T")) ")" )) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "S" ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) "T" ")" )) -> ($#v17_waybel_0 :::"infs-preserving"::: ) ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "S" ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) "T" ")" )) -> ($#v18_waybel_0 :::"sups-preserving"::: ) ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v17_waybel_0 :::"infs-preserving"::: ) ($#v22_waybel_0 :::"directed-sups-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v18_waybel_0 :::"sups-preserving"::: ) ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: WAYBEL34:43 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ))) ; theorem :: WAYBEL34:44 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" )) ")" )))) ; theorem :: WAYBEL34:45 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ))) ; theorem :: WAYBEL34:46 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool "ex" (Set (Var "g")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "g"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" )) ")" )))) ; theorem :: WAYBEL34:47 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow20 :::"Intersect"::: ) "(" (Set "(" (Set (Var "W")) ($#k4_waybel34 :::"-INF_category"::: ) ")" ) "," (Set "(" (Set (Var "W")) ($#k6_yellow21 :::"-UPS_category"::: ) ")" ) ")" ))) ; definitionlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; func "W" :::"-CL_category"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set "W" ($#k8_waybel34 :::"-INF(SC)_category"::: ) ) means :: WAYBEL34:def 12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k8_waybel34 :::"-INF(SC)_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" it) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" )); end; :: deftheorem defines :::"-CL_category"::: WAYBEL34:def 12 : (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k10_waybel34 :::"-CL_category"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" )) ")" ))); registrationlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "W" ($#k10_waybel34 :::"-CL_category"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#v3_yellow21 :::"with_complete_lattices"::: ) ; end; theorem :: WAYBEL34:48 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k10_waybel34 :::"-CL_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL34:49 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k10_waybel34 :::"-CL_category"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" )) ")" )))) ; definitionlet "W" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; func "W" :::"-CL-opp_category"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set "W" ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ) means :: WAYBEL34:def 13 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" "W" ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" it) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" )); end; :: deftheorem defines :::"-CL-opp_category"::: WAYBEL34:def 13 : (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_altcat_1 :::"strict"::: ) ($#v2_altcat_2 :::"full"::: ) ($#m1_altcat_2 :::"subcategory":::) "of" (Set (Set (Var "W")) ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k11_waybel34 :::"-CL-opp_category"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "b2"))) "iff" (Bool (Set ($#k4_yellow21 :::"latt"::: ) (Set (Var "a"))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" )) ")" ))); theorem :: WAYBEL34:50 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k11_waybel34 :::"-CL-opp_category"::: ) ")" )) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_orders_2 :::"strict"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL34:51 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" (Set (Var "W")) ($#k11_waybel34 :::"-CL-opp_category"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) )) "iff" (Bool "ex" (Set (Var "g")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_yellow21 :::"latt"::: ) (Set (Var "b")) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k2_waybel34 :::"UpperAdj"::: ) (Set (Var "g"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ")" )) ")" )))) ; theorem :: WAYBEL34:52 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) ) "," (Set (Set (Var "W")) ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Set (Var "W")) ($#k6_waybel34 :::"LowerAdj"::: ) ))) ; theorem :: WAYBEL34:53 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "W")) ($#k9_waybel34 :::"-SUP(SO)_category"::: ) ) "," (Set (Set (Var "W")) ($#k8_waybel34 :::"-INF(SC)_category"::: ) ) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Set (Var "W")) ($#k7_waybel34 :::"UpperAdj"::: ) ))) ; theorem :: WAYBEL34:54 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "W")) ($#k10_waybel34 :::"-CL_category"::: ) ) "," (Set (Set (Var "W")) ($#k11_waybel34 :::"-CL-opp_category"::: ) ) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Set (Var "W")) ($#k6_waybel34 :::"LowerAdj"::: ) ))) ; theorem :: WAYBEL34:55 (Bool "for" (Set (Var "W")) "being" ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "W")) ($#k11_waybel34 :::"-CL-opp_category"::: ) ) "," (Set (Set (Var "W")) ($#k10_waybel34 :::"-CL_category"::: ) ) ($#r3_yellow20 :::"are_anti-isomorphic_under"::: ) (Set (Set (Var "W")) ($#k7_waybel34 :::"UpperAdj"::: ) ))) ; begin definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"compact-preserving"::: means :: WAYBEL34:def 14 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_waybel_3 :::"compact"::: ) )) "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) "is" ($#v1_waybel_3 :::"compact"::: ) )); end; :: deftheorem defines :::"compact-preserving"::: WAYBEL34:def 14 : (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")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_waybel34 :::"compact-preserving"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_waybel_3 :::"compact"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) "is" ($#v1_waybel_3 :::"compact"::: ) )) ")" ))); theorem :: WAYBEL34:56 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v1_waybel34 :::"waybelow-preserving"::: ) )) "holds" (Bool (Set (Var "d")) "is" ($#v3_waybel34 :::"compact-preserving"::: ) ))) ; theorem :: WAYBEL34:57 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_waybel_8 :::"algebraic"::: ) ) & (Bool (Set (Var "d")) "is" ($#v3_waybel34 :::"compact-preserving"::: ) )) "holds" (Bool (Set (Var "d")) "is" ($#v1_waybel34 :::"waybelow-preserving"::: ) ))) ; theorem :: WAYBEL34:58 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))) & (Bool (Set (Var "g")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))))))) ; 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 :::"finite-sups-preserving"::: means :: WAYBEL34:def 15 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "S" "holds" (Bool "f" ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X")))); attr "f" is :::"bottom-preserving"::: means :: WAYBEL34:def 16 (Bool "f" ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set ($#k1_struct_0 :::"{}"::: ) "S")); end; :: deftheorem defines :::"finite-sups-preserving"::: WAYBEL34:def 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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X")))) ")" ))); :: deftheorem defines :::"bottom-preserving"::: WAYBEL34:def 16 : (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" ($#v5_waybel34 :::"bottom-preserving"::: ) ) "iff" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "S")))) ")" ))); theorem :: WAYBEL34:59 (Bool "for" (Set (Var "R")) "," (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 "R")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) )))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); redefine attr "f" is :::"bottom-preserving"::: means :: WAYBEL34:def 17 (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) "S" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "T")); end; :: deftheorem defines :::"bottom-preserving"::: WAYBEL34:def 17 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#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" ($#v5_waybel34 :::"bottom-preserving"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "T")))) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); attr "S" is :::"finite-sups-inheriting"::: means :: WAYBEL34:def 18 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "S" "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," "L")) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," "L" ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))); attr "S" is :::"bottom-inheriting"::: means :: WAYBEL34:def 19 (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) "L") ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")); end; :: deftheorem defines :::"finite-sups-inheriting"::: WAYBEL34:def 18 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_waybel34 :::"finite-sups-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))); :: deftheorem defines :::"bottom-inheriting"::: WAYBEL34:def 19 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_waybel34 :::"bottom-inheriting"::: ) ) "iff" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))); registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v18_waybel_0 :::"sups-preserving"::: ) -> ($#v5_waybel34 :::"bottom-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v6_waybel34 :::"finite-sups-inheriting"::: ) -> ($#v6_yellow_0 :::"join-inheriting"::: ) ($#v7_waybel34 :::"bottom-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v8_yellow_0 :::"sups-inheriting"::: ) -> ($#v6_waybel34 :::"finite-sups-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v18_waybel_0 :::"sups-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v4_yellow_0 :::"full"::: ) ($#v7_waybel34 :::"bottom-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v4_yellow_0 :::"full"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v8_yellow_0 :::"sups-inheriting"::: ) ($#v6_waybel34 :::"finite-sups-inheriting"::: ) ($#v7_waybel34 :::"bottom-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; theorem :: WAYBEL34:60 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v7_waybel34 :::"bottom-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#v4_yellow_0 :::"full"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) ($#v7_waybel34 :::"bottom-inheriting"::: ) -> ($#v4_yellow_0 :::"full"::: ) ($#v6_waybel34 :::"finite-sups-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; theorem :: WAYBEL34:61 (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")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v20_waybel_0 :::"join-preserving"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_waybel34 :::"bottom-preserving"::: ) ) ")" ))) ; theorem :: WAYBEL34:62 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v20_waybel_0 :::"join-preserving"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_waybel34 :::"bottom-preserving"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) ))) ; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v18_waybel_0 :::"sups-preserving"::: ) -> ($#v4_waybel34 :::"finite-sups-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v4_waybel34 :::"finite-sups-preserving"::: ) -> ($#v20_waybel_0 :::"join-preserving"::: ) ($#v5_waybel34 :::"bottom-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v18_waybel_0 :::"sups-preserving"::: ) ($#v4_waybel34 :::"finite-sups-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) "L") -> ($#v1_yellow_0 :::"lower-bounded"::: ) ; end; theorem :: WAYBEL34:63 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (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")) (Bool "for" (Set (Var "S9")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "T9")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T9"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9")))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S9")) "," (Set (Var "T9")))))))) ; theorem :: WAYBEL34:64 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v20_waybel_0 :::"join-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "S9")) "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 "S")) (Bool "for" (Set (Var "T9")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S9")) "," (Set (Var "T9")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9")))))) "holds" (Bool (Set (Var "g")) "is" ($#v20_waybel_0 :::"join-preserving"::: ) )))))) ; theorem :: WAYBEL34:65 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v4_waybel34 :::"finite-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "S9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v6_waybel34 :::"finite-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "T9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v6_waybel34 :::"finite-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S9")) "," (Set (Var "T9")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S9")))))) "holds" (Bool (Set (Var "g")) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) )))))) ; registrationlet "L" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k1_waybel_8 :::"CompactSublatt"::: ) "L") -> ($#v6_waybel34 :::"finite-sups-inheriting"::: ) ; end; theorem :: WAYBEL34:66 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#v18_waybel_0 :::"sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#v3_waybel34 :::"compact-preserving"::: ) ) "iff" (Bool (Set (Set (Var "d")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "T")) ")" ))) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "S")) ")" )) ")" ))) ; theorem :: WAYBEL34:67 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) "holds" (Bool "for" (Set (Var "g")) "being" ($#v17_waybel_0 :::"infs-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) "iff" (Bool (Set (Set "(" ($#k1_waybel34 :::"LowerAdj"::: ) (Set (Var "g")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "T")) ")" ))) "is" ($#v4_waybel34 :::"finite-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "S")) ")" )) ")" ))) ;