:: WAYBEL_5 semantic presentation begin theorem :: WAYBEL_5:1 (Bool "for" (Set (Var "L")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")) ")" ))) & (Bool "(" "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "I"))))) "holds" (Bool (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "I"))) ")" ) ")" )) ")" )) ; theorem :: WAYBEL_5:2 (Bool "for" (Set (Var "L")) "being" ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Semilattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "I")))) & (Bool "(" "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "J"))))) "holds" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) ")" ) ")" ))) ")" )) ; theorem :: WAYBEL_5:3 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L"))) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) )) ; theorem :: WAYBEL_5:4 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L"))) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; theorem :: WAYBEL_5:5 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Semilattice":::) "st" (Bool (Bool (Set ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L"))) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L"))) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) )) "holds" (Bool (Set ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L"))) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) )) ; definitionlet "J", "D" be ($#m1_hidden :::"set"::: ) ; let "K" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); mode DoubleIndexedSet of "K" "," "D" is ($#m2_pboole :::"ManySortedFunction"::: ) "of" "K" "," (Set "J" ($#k7_funcop_1 :::"-->"::: ) "D"); end; definitionlet "J" be ($#m1_hidden :::"set"::: ) ; let "K" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode DoubleIndexedSet of "K" "," "S" is ($#m2_pboole :::"DoubleIndexedSet":::) "of" "K" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"); end; theorem :: WAYBEL_5:6 (Bool "for" (Set (Var "J")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "D")) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "K")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set (Var "D"))))))) ; definitionlet "J", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "K" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Const "K")) "," (Set (Const "D")); let "j" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "J")); :: original: :::"."::: redefine func "F" :::"."::: "j" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "K" ($#k1_funct_1 :::"."::: ) "j" ")" ) "," "D"; end; registrationlet "J", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "K" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Const "K")) "," (Set (Const "D")); let "j" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "J")); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" "F" ($#k1_waybel_5 :::"."::: ) "j" ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "J" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "K" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); cluster -> bbbadV2_RELAT_1() for ($#m2_pboole :::"ManySortedFunction"::: ) "of" "K" "," (Set "J" ($#k7_funcop_1 :::"-->"::: ) "D"); end; theorem :: WAYBEL_5:7 (Bool "for" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" )))) "holds" (Bool (Set (Var "f")) "is" ($#m1_hidden :::"Function":::)))) ; theorem :: WAYBEL_5:8 (Bool "for" (Set (Var "F")) "being" ($#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 ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: WAYBEL_5:9 (Bool "for" (Set (Var "F")) "being" ($#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 ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" )))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: WAYBEL_5:10 (Bool "for" (Set (Var "J")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D"))))))) ; registrationlet "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k2_funct_6 :::"doms"::: ) "f") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionlet "J", "D" be ($#m1_hidden :::"set"::: ) ; let "K" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Const "K")) "," (Set (Const "D")); :: original: :::"Frege"::: redefine func :::"Frege"::: "F" -> ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) "F" ")" ) ")" ) ($#k7_funcop_1 :::"-->"::: ) "J") "," "D"; end; definitionlet "J", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "K" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Const "K")) "," (Set (Const "D")); let "G" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Const "F")) ")" ) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Const "J"))) "," (Set (Const "D")); let "f" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Const "F")) ")" )); :: original: :::"."::: redefine func "G" :::"."::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "J" "," "D"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); func :::"\//"::: "(" "F" "," "L" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "F" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") means :: WAYBEL_5:def 1 (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 it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"\\/"::: ) "(" (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," "L" ")" ))); func :::"/\\"::: "(" "F" "," "L" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "F" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") means :: WAYBEL_5:def 2 (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 it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," "L" ")" ))); end; :: deftheorem defines :::"\//"::: WAYBEL_5:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_5 :::"\//"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" )) "iff" (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 (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"\\/"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" ))) ")" )))); :: deftheorem defines :::"/\\"::: WAYBEL_5:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_5 :::"/\\"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" )) "iff" (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 (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" ))) ")" )))); notationlet "J" be ($#m1_hidden :::"set"::: ) ; let "K" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Const "K")) "," (Set (Const "L")); synonym :::"Sups"::: "F" for :::"\//"::: "(" "K" "," "J" ")" ; synonym :::"Infs"::: "F" for :::"/\\"::: "(" "K" "," "J" ")" ; end; notationlet "I", "J" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Set (Const "I")) ($#k7_funcop_1 :::"-->"::: ) (Set (Const "J"))) "," (Set (Const "L")); synonym :::"Sups"::: "F" for :::"\//"::: "(" "J" "," "I" ")" ; synonym :::"Infs"::: "F" for :::"/\\"::: "(" "J" "," "I" ")" ; end; theorem :: WAYBEL_5:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")))) & (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 ($#k4_yellow_2 :::"\\/"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"\\/"::: ) "(" (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" )) ")" )) "holds" (Bool (Set ($#k4_waybel_5 :::"\//"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k4_waybel_5 :::"\//"::: ) "(" (Set (Var "G")) "," (Set (Var "L")) ")" )))) ; theorem :: WAYBEL_5:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")))) & (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 ($#k5_yellow_2 :::"//\"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" )) ")" )) "holds" (Bool (Set ($#k5_waybel_5 :::"/\\"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k5_waybel_5 :::"/\\"::: ) "(" (Set (Var "G")) "," (Set (Var "L")) ")" )))) ; theorem :: WAYBEL_5:13 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_waybel_5 :::"\//"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ")" )))) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"\\/"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" )) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"\\/"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" )) ")" ))) "implies" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_waybel_5 :::"\//"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_waybel_5 :::"/\\"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ")" )))) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" )) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "L")) ")" )) ")" ))) "implies" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_waybel_5 :::"/\\"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ")" ))) ")" ")" )))) ; theorem :: WAYBEL_5:14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_waybel_5 :::"Sups"::: ) ")" )))) "implies" (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) ))) ")" & "(" (Bool (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) )))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_waybel_5 :::"Sups"::: ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_waybel_5 :::"Infs"::: ) ")" )))) "implies" (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"Inf"::: ) ))) ")" & "(" (Bool (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"Inf"::: ) )))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_waybel_5 :::"Infs"::: ) ")" ))) ")" ")" )))))) ; registrationlet "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "K" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Const "K")) "," (Set (Const "L")); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k4_waybel_5 :::"Sups"::: ) ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k5_waybel_5 :::"Infs"::: ) ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: WAYBEL_5:15 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" )))) "holds" (Bool (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set "(" (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")) ")" ) "," (Set (Var "L")) ")" ) ($#r3_orders_2 :::"<="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set ($#k4_yellow_2 :::"Sup"::: ) ) ($#r3_orders_2 :::"<="::: ) (Set (Var "a")))))) ; theorem :: WAYBEL_5:16 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_orders_2 :::">="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) )))))) ; theorem :: WAYBEL_5:17 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) ")" )) "holds" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))))) ; theorem :: WAYBEL_5:18 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool "(" "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "J")) ($#r2_hidden :::"in"::: ) (Set ($#k1_yellow_6 :::"the_universe_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) "holds" (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set (Set (Var "K")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_yellow_6 :::"the_universe_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) ")" )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" )) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" )) "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) )))) ")" )) "holds" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; theorem :: WAYBEL_5:19 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" )) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" )) "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) ))))) ")" )) ; definitionlet "J", "K", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "J")) "," (Set (Const "K")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "D")); :: original: :::"curry"::: redefine func :::"curry"::: "F" -> ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set "J" ($#k7_funcop_1 :::"-->"::: ) "K") "," "D"; end; theorem :: WAYBEL_5:20 (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "K")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "K")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_waybel_5 :::"curry"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "J"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k6_waybel_5 :::"curry"::: ) (Set (Var "F")) ")" ) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "K"))) & (Bool (Set (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_waybel_5 :::"curry"::: ) (Set (Var "F")) ")" ) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ))))) ; theorem :: WAYBEL_5:21 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "K")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set "(" ($#k6_waybel_5 :::"curry"::: ) (Set (Var "F")) ")" ) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" )) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" )) "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) )))) ")" )) ; theorem :: WAYBEL_5:22 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "K")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "ex" (Set (Var "f")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "J")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "K")) ")" ) ")" )) & (Bool "ex" (Set (Var "G")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "f")) "," (Set (Var "L")) "st" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "x")) ")" ))) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"Inf"::: ) )) ")" )) ")" )) "}" )) "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_orders_2 :::">="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")))))))) ; theorem :: WAYBEL_5:23 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "J")) "," (Set (Var "K")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "ex" (Set (Var "f")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "J")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "K")) ")" ) ")" )) & (Bool "ex" (Set (Var "G")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "f")) "," (Set (Var "L")) "st" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "x")) ")" ))) ")" ) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"Inf"::: ) )) ")" )) ")" )) "}" )) "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X"))))))) ")" )) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"completely-distributive"::: means :: WAYBEL_5:def 3 (Bool "(" (Bool "L" "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool "(" "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," "L" "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) )))) ")" ) ")" ); end; :: deftheorem defines :::"completely-distributive"::: WAYBEL_5:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_waybel_5 :::"completely-distributive"::: ) ) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool "(" "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_yellow_2 :::"Inf"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"Sup"::: ) )))) ")" ) ")" ) ")" )); registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_waybel_5 :::"completely-distributive"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_orders_2 :::"total"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_waybel_5 :::"completely-distributive"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: WAYBEL_5:24 (Bool "for" (Set (Var "L")) "being" ($#v1_waybel_5 :::"completely-distributive"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) ; registration cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_waybel_5 :::"completely-distributive"::: ) -> ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: WAYBEL_5:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")) ")" )) ($#r1_orders_2 :::">="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "Y"))))))) ; theorem :: WAYBEL_5:26 (Bool "for" (Set (Var "L")) "being" ($#v1_waybel_5 :::"completely-distributive"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "L")) ")" ))))) ; registration cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_waybel_5 :::"completely-distributive"::: ) -> ($#v9_waybel_1 :::"Heyting"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; mode CLSubFrame of "L" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v7_yellow_0 :::"infs-inheriting"::: ) ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; theorem :: WAYBEL_5:27 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k1_waybel_5 :::"."::: ) (Set (Var "j")) ")" )) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_waybel_5 :::"Infs"::: ) ")" )) "is" ($#v1_waybel_0 :::"directed"::: ) ))))) ; theorem :: WAYBEL_5:28 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"CLSubFrame":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "S")) "is" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::)))) ; theorem :: WAYBEL_5:29 (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"::: ) ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ))) "holds" (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::)))) ; notationlet "J", "y" be ($#m1_hidden :::"set"::: ) ; synonym "J" :::"=>"::: "y" for "J" :::"-->"::: "y"; end; registrationlet "J", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "J" ($#k2_funcop_1 :::"=>"::: ) "y") -> "J" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"J" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "A", "B", "J" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"=>"::: redefine func "J" :::"=>"::: "f" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "J" ($#k7_funcop_1 :::"-->"::: ) "A") "," (Set "J" ($#k7_funcop_1 :::"-->"::: ) "B"); end; theorem :: WAYBEL_5:30 (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "J")) ($#k7_waybel_5 :::"=>"::: ) (Set (Var "g")) ")" ) ($#k8_pboole :::"**"::: ) (Set "(" (Set (Var "J")) ($#k7_waybel_5 :::"=>"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "(" (Set (Var "J")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: WAYBEL_5:31 (Bool "for" (Set (Var "J")) "," (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "J")) ($#k7_waybel_5 :::"=>"::: ) (Set (Var "f")) ")" ) ($#k8_pboole :::"**"::: ) (Set (Var "F"))) "is" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "B")))))))) ; theorem :: WAYBEL_5:32 (Bool "for" (Set (Var "J")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set "(" (Set "(" (Set (Var "J")) ($#k7_waybel_5 :::"=>"::: ) (Set (Var "f")) ")" ) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F")))))))) ; theorem :: WAYBEL_5:33 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set (Var "g")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ))) "holds" (Bool (Set (Var "S")) "is" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::)))) ;