:: WAYBEL27 semantic presentation begin definitionlet "F" be ($#m1_hidden :::"Function":::); attr "F" is :::"uncurrying"::: means :: WAYBEL27:def 1 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool (Set (Var "x")) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::)) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")))) ")" ) ")" ); attr "F" is :::"currying"::: means :: WAYBEL27:def 2 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Function":::)) & (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Relation":::)) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")))) ")" ) ")" ); attr "F" is :::"commuting"::: means :: WAYBEL27:def 3 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool (Set (Var "x")) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::)) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")))) ")" ) ")" ); end; :: deftheorem defines :::"uncurrying"::: WAYBEL27:def 1 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_waybel27 :::"uncurrying"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "x")) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::)) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")))) ")" ) ")" ) ")" )); :: deftheorem defines :::"currying"::: WAYBEL27:def 2 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_waybel27 :::"currying"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Function":::)) & (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Relation":::)) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")))) ")" ) ")" ) ")" )); :: deftheorem defines :::"commuting"::: WAYBEL27:def 3 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_waybel27 :::"commuting"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "x")) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::)) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")))) ")" ) ")" ) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v1_waybel27 :::"uncurrying"::: ) ($#v2_waybel27 :::"currying"::: ) ($#v3_waybel27 :::"commuting"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_waybel27 :::"uncurrying"::: ) ($#v2_waybel27 :::"currying"::: ) ($#v3_waybel27 :::"commuting"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "F" be ($#v1_waybel27 :::"uncurrying"::: ) ($#m1_hidden :::"Function":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v1_waybel27 :::"uncurrying"::: ) ; end; registrationlet "F" be ($#v2_waybel27 :::"currying"::: ) ($#m1_hidden :::"Function":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v2_waybel27 :::"currying"::: ) ; end; theorem :: WAYBEL27:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_waybel27 :::"uncurrying"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) ")" ))) ; theorem :: WAYBEL27:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" ))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_waybel27 :::"currying"::: ) ) & "(" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "implies" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" )) ")" ")" ))) ; registrationlet "X", "Y", "Z" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" "Y" "," "Z" ")" ")" ) ")" ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" "Y" "," "Z" ")" ")" ) ")" )) ($#v1_waybel27 :::"uncurrying"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) "," "Z" ")" ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) "," "Z" ")" )) ($#v2_waybel27 :::"currying"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: WAYBEL27:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v3_waybel27 :::"commuting"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))))) ; theorem :: WAYBEL27:4 (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_waybel27 :::"uncurrying"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#v2_waybel27 :::"currying"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: WAYBEL27:5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_waybel27 :::"currying"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#v1_waybel27 :::"uncurrying"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "C")) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))))) ; theorem :: WAYBEL27:6 (Bool "for" (Set (Var "f")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_card_3 :::"pi"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" ) "," (Set (Var "i")) ")" )))) ; theorem :: WAYBEL27:7 (Bool "for" (Set (Var "f")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set ($#k5_card_3 :::"pi"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")))))) ; theorem :: WAYBEL27:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_3 :::"pi"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" ) "," (Set (Var "i")) ")" ))))) ; theorem :: WAYBEL27:9 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k5_card_3 :::"pi"::: ) "(" (Set "(" (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; registrationlet "T" be ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") -> ($#v4_funct_1 :::"functional"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) bbbadV1_LATTICE3() bbbadV2_LATTICE3() ($#v3_lattice3 :::"complete"::: ) ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) for ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "T"; end; theorem :: WAYBEL27:10 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v11_quantal1 :::"idempotent"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))))) ; theorem :: WAYBEL27:11 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "T1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "T")) "is" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T1")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T1")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "f1")))) "holds" (Bool (Set (Var "f1")) "is" ($#v5_orders_3 :::"monotone"::: ) )))) ; theorem :: WAYBEL27:12 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "T1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "T1")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T1")) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "f1")))) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )))) ; theorem :: WAYBEL27:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_funct_3 :::"chi"::: ) "(" (Set (Var "V")) "," (Set (Var "X")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "V"))) & (Bool (Set (Set "(" ($#k5_funct_3 :::"chi"::: ) "(" (Set (Var "V")) "," (Set (Var "X")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "V")))) ")" ))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Const "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Const "X")) ")" ); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "T"; end; theorem :: WAYBEL27:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_orders_2 :::"<="::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k1_waybel27 :::"."::: ) (Set (Var "x"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "g")) ($#k1_waybel27 :::"."::: ) (Set (Var "x"))))) ")" )))) ; theorem :: WAYBEL27:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "," (Set (Var "S")) "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 "L"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) "#)" ) ($#r1_hidden :::"="::: ) (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"))) "#)" ))) "holds" (Bool (Set (Set (Var "L")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL27:16 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S2"))) "#)" )) & (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2"))) "#)" ))) "holds" (Bool (Set ($#k1_waybel26 :::"oContMaps"::: ) "(" (Set (Var "S1")) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel26 :::"oContMaps"::: ) "(" (Set (Var "S2")) "," (Set (Var "T2")) ")" ))) ; theorem :: WAYBEL27:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set (Var "Y")) "," (Set (Var "X")) ")" )) ")" ) ")" ))) ; theorem :: WAYBEL27:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X"))) "," (Set (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) ; theorem :: WAYBEL27:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y"))) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_waybel27 :::"commuting"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v5_orders_3 :::"monotone"::: ) )))))) ; theorem :: WAYBEL27:20 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_waybel27 :::"uncurrying"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v5_orders_3 :::"monotone"::: ) )))))) ; theorem :: WAYBEL27:21 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S2")) "," (Set (Var "S1")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_waybel27 :::"currying"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v5_orders_3 :::"monotone"::: ) )))))) ; begin definitionlet "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"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"UPS"::: "(" "S" "," "T" ")" -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) means :: WAYBEL27:def 4 (Bool "(" (Bool it "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set "T" ($#k6_yellow_1 :::"|^"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "iff" (Bool (Set (Var "x")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" "S" "," "T") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"UPS"::: WAYBEL27:def 4 : (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 "b3")) "being" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b3")) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3")))) "iff" (Bool (Set (Var "x")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" ) ")" ) ")" ) ")" )))); 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"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_waybel27 :::"UPS"::: ) "(" "S" "," "T" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ; 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"::: ) ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k2_waybel27 :::"UPS"::: ) "(" "S" "," "T" ")" ) -> ($#v1_orders_2 :::"strict"::: ) ($#v4_orders_2 :::"transitive"::: ) ; end; theorem :: WAYBEL27:22 (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"::: ) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" )))) ; definitionlet "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"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Const "S")) "," (Set (Const "T")) ")" ")" ); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); :: original: :::"."::: redefine func "f" :::"."::: "s" -> ($#m1_subset_1 :::"Element":::) "of" "T"; end; theorem :: WAYBEL27:23 (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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_orders_2 :::"<="::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k3_waybel27 :::"."::: ) (Set (Var "s"))) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "g")) ($#k3_waybel27 :::"."::: ) (Set (Var "s"))))) ")" )))) ; theorem :: WAYBEL27:24 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel17 :::"SCMaps"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ))) ; theorem :: WAYBEL27:25 (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#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 (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S9")) "," (Set (Var "T9")) ")" )))) ; registrationlet "S", "T" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k2_waybel27 :::"UPS"::: ) "(" "S" "," "T" ")" ) -> ($#v1_orders_2 :::"strict"::: ) ($#v3_lattice3 :::"complete"::: ) ; end; theorem :: WAYBEL27:26 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))))) ; theorem :: WAYBEL27:27 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ")" ) ")" )))) ; definitionlet "S1", "S2", "T1", "T2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S1")) "," (Set (Const "S2")); assume (Bool (Set (Const "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ; let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T1")) "," (Set (Const "T2")); assume (Bool (Set (Const "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) ; func :::"UPS"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" "S2" "," "T1" ")" ")" ) "," (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" "S1" "," "T2" ")" ")" ) means :: WAYBEL27:def 5 (Bool "for" (Set (Var "h")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" "S2" "," "T1" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "g" ($#k1_partfun1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k1_partfun1 :::"*"::: ) "f"))); end; :: deftheorem defines :::"UPS"::: WAYBEL27:def 5 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S2")) "," (Set (Var "T1")) ")" ")" ) "," (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S1")) "," (Set (Var "T2")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel27 :::"UPS"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "for" (Set (Var "h")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S2")) "," (Set (Var "T1")) "holds" (Bool (Set (Set (Var "b7")) ($#k1_funct_1 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))) ")" ))))); theorem :: WAYBEL27:28 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "," (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "T3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f1")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S2")) "," (Set (Var "S3")) (Bool "for" (Set (Var "f2")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) (Bool "for" (Set (Var "g1")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) (Bool "for" (Set (Var "g2")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T2")) "," (Set (Var "T3")) "holds" (Bool (Set (Set "(" ($#k4_waybel27 :::"UPS"::: ) "(" (Set (Var "f2")) "," (Set (Var "g2")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_waybel27 :::"UPS"::: ) "(" (Set (Var "f1")) "," (Set (Var "g1")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k4_waybel27 :::"UPS"::: ) "(" (Set "(" (Set (Var "f1")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f2")) ")" ) "," (Set "(" (Set (Var "g2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g1")) ")" ) ")" ))))))) ; theorem :: WAYBEL27:29 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k4_waybel27 :::"UPS"::: ) "(" (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "T")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" )))) ; theorem :: WAYBEL27:30 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) (Bool "for" (Set (Var "g")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool (Set ($#k4_waybel27 :::"UPS"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )))) ; theorem :: WAYBEL27:31 (Bool (Set ($#k1_waybel25 :::"Omega"::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) )) "is" ($#v4_waybel11 :::"Scott"::: ) ) ; theorem :: WAYBEL27:32 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set ($#k1_waybel26 :::"oContMaps"::: ) "(" (Set (Var "S")) "," (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ")" ))) ; theorem :: WAYBEL27:33 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ")" ")" ) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) & (Bool "(" "for" (Set (Var "f")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))) ")" ) ")" ))) ; theorem :: WAYBEL27:34 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ) ")" ) "," (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S")) ")" )) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) ; theorem :: WAYBEL27:35 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) & (Bool (Set (Var "g")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool (Set ($#k4_waybel27 :::"UPS"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )))) ; theorem :: WAYBEL27:36 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r5_waybel_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "T1")) "," (Set (Var "T2")) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S2")) "," (Set (Var "T1")) ")" ) "," (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S1")) "," (Set (Var "T2")) ")" ) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) ; theorem :: WAYBEL27:37 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#v6_waybel_1 :::"projection"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set "(" ($#k4_waybel27 :::"UPS"::: ) "(" (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "S")) ")" ) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" ) ")" )))) ; theorem :: WAYBEL27:38 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))))))) ; theorem :: WAYBEL27:39 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" )))))) ; theorem :: WAYBEL27:40 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" )) "holds" (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ))))) ; theorem :: WAYBEL27:41 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_waybel27 :::"commuting"::: ) ) & (Bool (Set (Var "F")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) ")" )))) ; theorem :: WAYBEL27:42 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) ($#r5_waybel_1 :::"are_isomorphic"::: ) ))) ; theorem :: WAYBEL27:43 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; theorem :: WAYBEL27:44 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v2_waybel_8 :::"algebraic"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is" ($#v2_waybel_8 :::"algebraic"::: ) )) ; theorem :: WAYBEL27:45 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) "holds" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))))) ; theorem :: WAYBEL27:46 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T")) "holds" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" )))) ; theorem :: WAYBEL27:47 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k2_waybel27 :::"UPS"::: ) "(" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_waybel27 :::"uncurrying"::: ) ) & (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) ")" ))) ;