:: CLOSURE2 semantic presentation begin notationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); synonym "A" :::"in'"::: "B" for "A" :::"in"::: "B"; end; notationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); synonym "A" :::"c='"::: "B" for "A" :::"c="::: "B"; end; theorem :: CLOSURE2:1 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "Y")))))) ; theorem :: CLOSURE2:2 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k5_mssubfam :::"bool"::: ) (Set (Var "A")) ")" ) ")" )))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"Bool"::: "M" -> ($#m1_hidden :::"set"::: ) means :: CLOSURE2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M") ")" )); end; :: deftheorem defines :::"Bool"::: CLOSURE2:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_closure2 :::"Bool"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M"))) ")" )) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k1_closure2 :::"Bool"::: ) "M") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v2_card_3 :::"with_common_domain"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode SubsetFamily of "M" is ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" ); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"Bool"::: redefine func :::"Bool"::: "M" -> ($#m1_subset_1 :::"SubsetFamily":::) "of" "M"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v2_card_3 :::"with_common_domain"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_xboole_0 :::"empty"::: ) ($#v4_funct_1 :::"functional"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "S" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M"; end; theorem :: CLOSURE2:3 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "," (Set (Var "SG")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "SG"))) "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: CLOSURE2:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "," (Set (Var "SG")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "SG"))) "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: CLOSURE2:5 (Bool "for" (Set (Var "I")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k7_subset_1 :::"\"::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: CLOSURE2:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "," (Set (Var "SG")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "SG"))) "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: CLOSURE2:7 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M"))))) ; theorem :: CLOSURE2:8 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "M")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r2_pboole :::"c="::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M"))))) ; theorem :: CLOSURE2:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "E")) ($#k3_pboole :::"/\"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))))))) ; theorem :: CLOSURE2:10 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "E")) ($#k2_pboole :::"\/"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))))))) ; theorem :: CLOSURE2:11 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "E")) ($#k4_pboole :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))))))) ; theorem :: CLOSURE2:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "E")) ($#k5_pboole :::"\+\"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))))))) ; begin definitionlet "S" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; func :::"|.":::"S":::".|"::: -> ($#m1_hidden :::"Function":::) means :: CLOSURE2:def 2 (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "S") & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool verum) "}" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool verum) "}" ) ")" ) ")" )) if (Bool "S" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"|."::: CLOSURE2:def 2 : (Bool "for" (Set (Var "S")) "being" ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_closure2 :::"|."::: ) (Set (Var "S")) ($#k3_closure2 :::".|"::: ) )) "iff" (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool verum) "}" )) & (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 "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) : (Bool verum) "}" ) ")" ) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_closure2 :::"|."::: ) (Set (Var "S")) ($#k3_closure2 :::".|"::: ) )) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))); theorem :: CLOSURE2:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_closure2 :::"|."::: ) (Set (Var "SF")) ($#k3_closure2 :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "I")))))) ; registrationlet "S" be ($#v1_xboole_0 :::"empty"::: ) ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_closure2 :::"|."::: ) "S" ($#k3_closure2 :::".|"::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "S" be ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); func :::"|:":::"S":::":|"::: -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" equals :: CLOSURE2:def 3 (Set ($#k3_closure2 :::"|."::: ) "S" ($#k3_closure2 :::".|"::: ) ) if (Bool "S" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Set ($#k1_pboole :::"[[0]]"::: ) "I"); end; :: deftheorem defines :::"|:"::: CLOSURE2:def 3 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k4_closure2 :::"|:"::: ) (Set (Var "S")) ($#k4_closure2 :::":|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_closure2 :::"|."::: ) (Set (Var "S")) ($#k3_closure2 :::".|"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool (Set ($#k4_closure2 :::"|:"::: ) (Set (Var "S")) ($#k4_closure2 :::":|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) ")" ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "S" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); cluster (Set ($#k4_closure2 :::"|:"::: ) "S" ($#k4_closure2 :::":|"::: ) ) -> bbbadV3_RELAT_1() ; end; theorem :: CLOSURE2:14 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set (Var "SF")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set ($#k4_closure2 :::"|:"::: ) (Set (Var "SF")) ($#k4_closure2 :::":|"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where x "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "SF"))) "}" ))))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "SF" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); cluster (Set ($#k4_closure2 :::"|:"::: ) "SF" ($#k4_closure2 :::":|"::: ) ) -> bbbadV2_RELAT_1() ; end; theorem :: CLOSURE2:15 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_closure2 :::"|."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k3_closure2 :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ; theorem :: CLOSURE2:16 (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_closure2 :::"|."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "f1")) ($#k2_tarski :::"}"::: ) ) ($#k3_closure2 :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" )))) ; theorem :: CLOSURE2:17 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set ($#k3_closure2 :::"|."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) ($#k3_closure2 :::".|"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: CLOSURE2:18 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "SF")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set ($#k4_closure2 :::"|:"::: ) (Set (Var "SF")) ($#k4_closure2 :::":|"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: CLOSURE2:19 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_closure2 :::"|."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "f1")) ($#k2_tarski :::"}"::: ) ) ($#k3_closure2 :::".|"::: ) )))) "holds" (Bool (Set (Set ($#k3_closure2 :::"|."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "f1")) ($#k2_tarski :::"}"::: ) ) ($#k3_closure2 :::".|"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) )))) ; theorem :: CLOSURE2:20 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "SF")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "f1")) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set ($#k4_closure2 :::"|:"::: ) (Set (Var "SF")) ($#k4_closure2 :::":|"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) )))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "SF" be ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); :: original: :::"|:"::: redefine func :::"|:":::"SF":::":|"::: -> ($#m3_pboole :::"MSSubsetFamily":::) "of" "M"; end; theorem :: CLOSURE2:21 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "SF")))) "holds" (Bool (Set (Var "A")) ($#r1_pboole :::"in'"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "SF")) ($#k5_closure2 :::":|"::: ) ))))) ; theorem :: CLOSURE2:22 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "SF")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "SF")) ($#k5_closure2 :::":|"::: ) )) ($#r6_pboole :::"="::: ) (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "B"))))))) ; theorem :: CLOSURE2:23 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "SF")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "E")) "," (Set (Var "T")) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "SF")) ($#k5_closure2 :::":|"::: ) )) ($#r6_pboole :::"="::: ) (Set (Set (Var "E")) ($#k3_pboole :::"/\"::: ) (Set (Var "T")))))))) ; theorem :: CLOSURE2:24 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "Z")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "Z1")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "Z1")) ($#r2_hidden :::"in"::: ) (Set (Var "SF")))) "holds" (Bool (Set (Var "Z")) ($#r2_pboole :::"c='"::: ) (Set (Var "Z1"))) ")" )) "holds" (Bool (Set (Var "Z")) ($#r2_pboole :::"c='"::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "SF")) ($#k5_closure2 :::":|"::: ) ))))))) ; theorem :: CLOSURE2:25 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k5_closure2 :::"|:"::: ) (Set "(" ($#k2_closure2 :::"Bool"::: ) (Set (Var "M")) ")" ) ($#k5_closure2 :::":|"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k5_mssubfam :::"bool"::: ) (Set (Var "M")))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "IT" be ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); attr "IT" is :::"additive"::: means :: CLOSURE2:def 4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "I" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) "IT")); attr "IT" is :::"absolutely-additive"::: means :: CLOSURE2:def 5 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" "M" "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) "IT")) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) )) ($#r2_hidden :::"in"::: ) "IT")); attr "IT" is :::"multiplicative"::: means :: CLOSURE2:def 6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "I" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) "IT")); attr "IT" is :::"absolutely-multiplicative"::: means :: CLOSURE2:def 7 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" "M" "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) "IT")) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) )) ($#r2_hidden :::"in"::: ) "IT")); attr "IT" is :::"properly-upper-bound"::: means :: CLOSURE2:def 8 (Bool "M" ($#r2_hidden :::"in"::: ) "IT"); attr "IT" is :::"properly-lower-bound"::: means :: CLOSURE2:def 9 (Bool (Set ($#k1_pboole :::"[[0]]"::: ) "I") ($#r2_hidden :::"in"::: ) "IT"); end; :: deftheorem defines :::"additive"::: CLOSURE2:def 4 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_closure2 :::"additive"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"absolutely-additive"::: CLOSURE2:def 5 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_closure2 :::"absolutely-additive"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"multiplicative"::: CLOSURE2:def 6 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_closure2 :::"multiplicative"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"absolutely-multiplicative"::: CLOSURE2:def 7 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_closure2 :::"absolutely-multiplicative"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"properly-upper-bound"::: CLOSURE2:def 8 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_closure2 :::"properly-upper-bound"::: ) ) "iff" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) ")" )))); :: deftheorem defines :::"properly-lower-bound"::: CLOSURE2:def 9 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_closure2 :::"properly-lower-bound"::: ) ) "iff" (Bool (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v2_card_3 :::"with_common_domain"::: ) ($#v1_closure2 :::"additive"::: ) ($#v2_closure2 :::"absolutely-additive"::: ) ($#v3_closure2 :::"multiplicative"::: ) ($#v4_closure2 :::"absolutely-multiplicative"::: ) ($#v5_closure2 :::"properly-upper-bound"::: ) ($#v6_closure2 :::"properly-lower-bound"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); :: original: :::"Bool"::: redefine func :::"Bool"::: "M" -> ($#v1_closure2 :::"additive"::: ) ($#v2_closure2 :::"absolutely-additive"::: ) ($#v3_closure2 :::"multiplicative"::: ) ($#v4_closure2 :::"absolutely-multiplicative"::: ) ($#v5_closure2 :::"properly-upper-bound"::: ) ($#v6_closure2 :::"properly-lower-bound"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" "M"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v2_closure2 :::"absolutely-additive"::: ) -> ($#v1_closure2 :::"additive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v4_closure2 :::"absolutely-multiplicative"::: ) -> ($#v3_closure2 :::"multiplicative"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v4_closure2 :::"absolutely-multiplicative"::: ) -> ($#v5_closure2 :::"properly-upper-bound"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v5_closure2 :::"properly-upper-bound"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v2_closure2 :::"absolutely-additive"::: ) -> ($#v6_closure2 :::"properly-lower-bound"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v6_closure2 :::"properly-lower-bound"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_closure2 :::"Bool"::: ) "M" ")" )); end; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode SetOp of "M" is ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ) "," (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "f" be ($#m1_subset_1 :::"SetOp":::) "of" (Set (Const "M")); let "x" be ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Const "M"))); :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M"); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "IT" be ($#m1_subset_1 :::"SetOp":::) "of" (Set (Const "M")); attr "IT" is :::"reflexive"::: means :: CLOSURE2:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M") "holds" (Bool (Set (Var "x")) ($#r2_pboole :::"c='"::: ) (Set "IT" ($#k7_closure2 :::"."::: ) (Set (Var "x"))))); attr "IT" is :::"monotonic"::: means :: CLOSURE2:def 11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M") "st" (Bool (Bool (Set (Var "x")) ($#r2_pboole :::"c='"::: ) (Set (Var "y")))) "holds" (Bool (Set "IT" ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r2_pboole :::"c='"::: ) (Set "IT" ($#k7_closure2 :::"."::: ) (Set (Var "y"))))); attr "IT" is :::"idempotent"::: means :: CLOSURE2:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M") "holds" (Bool (Set "IT" ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set "IT" ($#k7_closure2 :::"."::: ) (Set "(" "IT" ($#k7_closure2 :::"."::: ) (Set (Var "x")) ")" )))); attr "IT" is :::"topological"::: means :: CLOSURE2:def 13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M") "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_pboole :::"\/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "IT" ($#k7_closure2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" "IT" ($#k7_closure2 :::"."::: ) (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"reflexive"::: CLOSURE2:def 10 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_closure2 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Var "x")) ($#r2_pboole :::"c='"::: ) (Set (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))))) ")" )))); :: deftheorem defines :::"monotonic"::: CLOSURE2:def 11 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_closure2 :::"monotonic"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_pboole :::"c='"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r2_pboole :::"c='"::: ) (Set (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set (Var "y"))))) ")" )))); :: deftheorem defines :::"idempotent"::: CLOSURE2:def 12 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_closure2 :::"idempotent"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set "(" (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))); :: deftheorem defines :::"topological"::: CLOSURE2:def 13 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_closure2 :::"topological"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_pboole :::"\/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_pboole :::"\/"::: ) (Set "(" (Set (Var "IT")) ($#k7_closure2 :::"."::: ) (Set (Var "y")) ")" )))) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k6_closure2 :::"Bool"::: ) "M")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v7_closure2 :::"reflexive"::: ) ($#v8_closure2 :::"monotonic"::: ) ($#v9_closure2 :::"idempotent"::: ) ($#v10_closure2 :::"topological"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ) "," (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: CLOSURE2:26 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k6_closure2 :::"Bool"::: ) (Set (Var "A")) ")" )) "is" ($#v7_closure2 :::"reflexive"::: ) ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE2:27 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k6_closure2 :::"Bool"::: ) (Set (Var "A")) ")" )) "is" ($#v8_closure2 :::"monotonic"::: ) ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE2:28 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k6_closure2 :::"Bool"::: ) (Set (Var "A")) ")" )) "is" ($#v9_closure2 :::"idempotent"::: ) ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE2:29 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k6_closure2 :::"Bool"::: ) (Set (Var "A")) ")" )) "is" ($#v10_closure2 :::"topological"::: ) ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "A"))))) ; theorem :: CLOSURE2:30 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "E")) ($#r6_pboole :::"="::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) "is" ($#v7_closure2 :::"reflexive"::: ) )) "holds" (Bool (Set (Var "E")) ($#r6_pboole :::"="::: ) (Set (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "E")))))))) ; theorem :: CLOSURE2:31 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v7_closure2 :::"reflexive"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "holds" (Bool (Set (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "X"))) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "g")) "is" ($#v9_closure2 :::"idempotent"::: ) )))) ; theorem :: CLOSURE2:32 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set (Set (Var "E")) ($#k3_pboole :::"/\"::: ) (Set (Var "T")))) & (Bool (Set (Var "g")) "is" ($#v8_closure2 :::"monotonic"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "A"))) ($#r2_pboole :::"c="::: ) (Set (Set "(" (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "E")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "T")) ")" )))))))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v10_closure2 :::"topological"::: ) -> ($#v8_closure2 :::"monotonic"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ) "," (Set "(" ($#k6_closure2 :::"Bool"::: ) "M" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: CLOSURE2:33 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "," (Set (Var "T")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k2_closure2 :::"Bool"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set (Set (Var "E")) ($#k4_pboole :::"\"::: ) (Set (Var "T")))) & (Bool (Set (Var "g")) "is" ($#v10_closure2 :::"topological"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "E")) ")" ) ($#k4_pboole :::"\"::: ) (Set "(" (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "T")) ")" )) ($#r2_pboole :::"c="::: ) (Set (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "A"))))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "h", "g" be ($#m1_subset_1 :::"SetOp":::) "of" (Set (Const "M")); :: original: :::"*"::: redefine func "g" :::"*"::: "h" -> ($#m1_subset_1 :::"SetOp":::) "of" "M"; end; theorem :: CLOSURE2:34 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v7_closure2 :::"reflexive"::: ) ) & (Bool (Set (Var "h")) "is" ($#v7_closure2 :::"reflexive"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k8_closure2 :::"*"::: ) (Set (Var "h"))) "is" ($#v7_closure2 :::"reflexive"::: ) )))) ; theorem :: CLOSURE2:35 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v8_closure2 :::"monotonic"::: ) ) & (Bool (Set (Var "h")) "is" ($#v8_closure2 :::"monotonic"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k8_closure2 :::"*"::: ) (Set (Var "h"))) "is" ($#v8_closure2 :::"monotonic"::: ) )))) ; theorem :: CLOSURE2:36 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v9_closure2 :::"idempotent"::: ) ) & (Bool (Set (Var "h")) "is" ($#v9_closure2 :::"idempotent"::: ) ) & (Bool (Set (Set (Var "g")) ($#k8_closure2 :::"*"::: ) (Set (Var "h"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "h")) ($#k8_closure2 :::"*"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k8_closure2 :::"*"::: ) (Set (Var "h"))) "is" ($#v9_closure2 :::"idempotent"::: ) )))) ; theorem :: CLOSURE2:37 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v10_closure2 :::"topological"::: ) ) & (Bool (Set (Var "h")) "is" ($#v10_closure2 :::"topological"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k8_closure2 :::"*"::: ) (Set (Var "h"))) "is" ($#v10_closure2 :::"topological"::: ) )))) ; begin definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "c2" is :::"strict"::: ; struct :::"ClosureStr"::: "over" "S" -> ($#l2_msualg_1 :::"many-sorted"::: ) "over" "S"; aggr :::"ClosureStr":::(# :::"Sorts":::, :::"Family"::: #) -> ($#l1_closure2 :::"ClosureStr"::: ) "over" "S"; sel :::"Family"::: "c2" -> ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "c2"); end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "IT" be ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Const "S")); attr "IT" is :::"additive"::: means :: CLOSURE2:def 14 (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "IT") "is" ($#v1_closure2 :::"additive"::: ) ); attr "IT" is :::"absolutely-additive"::: means :: CLOSURE2:def 15 (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "IT") "is" ($#v2_closure2 :::"absolutely-additive"::: ) ); attr "IT" is :::"multiplicative"::: means :: CLOSURE2:def 16 (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "IT") "is" ($#v3_closure2 :::"multiplicative"::: ) ); attr "IT" is :::"absolutely-multiplicative"::: means :: CLOSURE2:def 17 (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "IT") "is" ($#v4_closure2 :::"absolutely-multiplicative"::: ) ); attr "IT" is :::"properly-upper-bound"::: means :: CLOSURE2:def 18 (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "IT") "is" ($#v5_closure2 :::"properly-upper-bound"::: ) ); attr "IT" is :::"properly-lower-bound"::: means :: CLOSURE2:def 19 (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "IT") "is" ($#v6_closure2 :::"properly-lower-bound"::: ) ); end; :: deftheorem defines :::"additive"::: CLOSURE2:def 14 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v12_closure2 :::"additive"::: ) ) "iff" (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v1_closure2 :::"additive"::: ) ) ")" ))); :: deftheorem defines :::"absolutely-additive"::: CLOSURE2:def 15 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v13_closure2 :::"absolutely-additive"::: ) ) "iff" (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v2_closure2 :::"absolutely-additive"::: ) ) ")" ))); :: deftheorem defines :::"multiplicative"::: CLOSURE2:def 16 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v14_closure2 :::"multiplicative"::: ) ) "iff" (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v3_closure2 :::"multiplicative"::: ) ) ")" ))); :: deftheorem defines :::"absolutely-multiplicative"::: CLOSURE2:def 17 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v15_closure2 :::"absolutely-multiplicative"::: ) ) "iff" (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v4_closure2 :::"absolutely-multiplicative"::: ) ) ")" ))); :: deftheorem defines :::"properly-upper-bound"::: CLOSURE2:def 18 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v16_closure2 :::"properly-upper-bound"::: ) ) "iff" (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v5_closure2 :::"properly-upper-bound"::: ) ) ")" ))); :: deftheorem defines :::"properly-lower-bound"::: CLOSURE2:def 19 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v17_closure2 :::"properly-lower-bound"::: ) ) "iff" (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "IT"))) "is" ($#v6_closure2 :::"properly-lower-bound"::: ) ) ")" ))); definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); func :::"Full"::: "MS" -> ($#l1_closure2 :::"ClosureStr"::: ) "over" "S" equals :: CLOSURE2:def 20 (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," (Set "(" ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") ")" ) "#)" ); end; :: deftheorem defines :::"Full"::: CLOSURE2:def 20 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "MS")) "being" ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Var "S")) "holds" (Bool (Set ($#k9_closure2 :::"Full"::: ) (Set (Var "MS"))) ($#r1_hidden :::"="::: ) (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MS"))) "," (Set "(" ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "MS"))) ")" ) "#)" )))); registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); cluster (Set ($#k9_closure2 :::"Full"::: ) "MS") -> ($#v11_closure2 :::"strict"::: ) ($#v12_closure2 :::"additive"::: ) ($#v13_closure2 :::"absolutely-additive"::: ) ($#v14_closure2 :::"multiplicative"::: ) ($#v15_closure2 :::"absolutely-multiplicative"::: ) ($#v16_closure2 :::"properly-upper-bound"::: ) ($#v17_closure2 :::"properly-lower-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); cluster (Set ($#k9_closure2 :::"Full"::: ) "MS") -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v4_msualg_1 :::"non-empty"::: ) ($#v11_closure2 :::"strict"::: ) ($#v12_closure2 :::"additive"::: ) ($#v13_closure2 :::"absolutely-additive"::: ) ($#v14_closure2 :::"multiplicative"::: ) ($#v15_closure2 :::"absolutely-multiplicative"::: ) ($#v16_closure2 :::"properly-upper-bound"::: ) ($#v17_closure2 :::"properly-lower-bound"::: ) for ($#l1_closure2 :::"ClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v12_closure2 :::"additive"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "CS") -> ($#v1_closure2 :::"additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v13_closure2 :::"absolutely-additive"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "CS") -> ($#v2_closure2 :::"absolutely-additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v14_closure2 :::"multiplicative"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "CS") -> ($#v3_closure2 :::"multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v15_closure2 :::"absolutely-multiplicative"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "CS") -> ($#v4_closure2 :::"absolutely-multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v16_closure2 :::"properly-upper-bound"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "CS") -> ($#v5_closure2 :::"properly-upper-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "CS" be ($#v17_closure2 :::"properly-lower-bound"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Const "S")); cluster (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "CS") -> ($#v6_closure2 :::"properly-lower-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "M" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "F" be ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set (Const "M")); cluster (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" "M" "," "F" "#)" ) -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v1_closure2 :::"additive"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v12_closure2 :::"additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v2_closure2 :::"absolutely-additive"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v13_closure2 :::"absolutely-additive"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v3_closure2 :::"multiplicative"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v14_closure2 :::"multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v4_closure2 :::"absolutely-multiplicative"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v15_closure2 :::"absolutely-multiplicative"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v5_closure2 :::"properly-upper-bound"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v16_closure2 :::"properly-upper-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "MS" be ($#l2_msualg_1 :::"many-sorted"::: ) "over" (Set (Const "S")); let "F" be ($#v6_closure2 :::"properly-lower-bound"::: ) ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "MS"))); cluster (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "MS") "," "F" "#)" ) -> ($#v17_closure2 :::"properly-lower-bound"::: ) ; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v13_closure2 :::"absolutely-additive"::: ) -> ($#v12_closure2 :::"additive"::: ) for ($#l1_closure2 :::"ClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v15_closure2 :::"absolutely-multiplicative"::: ) -> ($#v14_closure2 :::"multiplicative"::: ) for ($#l1_closure2 :::"ClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v15_closure2 :::"absolutely-multiplicative"::: ) -> ($#v16_closure2 :::"properly-upper-bound"::: ) for ($#l1_closure2 :::"ClosureStr"::: ) "over" "S"; end; registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v13_closure2 :::"absolutely-additive"::: ) -> ($#v17_closure2 :::"properly-lower-bound"::: ) for ($#l1_closure2 :::"ClosureStr"::: ) "over" "S"; end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode ClosureSystem of "S" is ($#v15_closure2 :::"absolutely-multiplicative"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" "S"; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode ClosureOperator of "M" is ($#v7_closure2 :::"reflexive"::: ) ($#v8_closure2 :::"monotonic"::: ) ($#v9_closure2 :::"idempotent"::: ) ($#m1_subset_1 :::"SetOp":::) "of" "M"; end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "g" be ($#m1_subset_1 :::"ClosureOperator":::) "of" (Set (Const "A")); func :::"ClOp->ClSys"::: "g" -> ($#v11_closure2 :::"strict"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" "S" means :: CLOSURE2:def 21 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r6_pboole :::"="::: ) "A") & (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "A") : (Bool (Set "g" ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set (Var "x"))) "}" ) ")" ); end; :: deftheorem defines :::"ClOp->ClSys"::: CLOSURE2:def 21 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"ClosureOperator":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#v11_closure2 :::"strict"::: ) ($#l1_closure2 :::"ClosureStr"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_closure2 :::"ClOp->ClSys"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b4"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))) & (Bool (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set (Var "A"))) : (Bool (Set (Set (Var "g")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set (Var "x"))) "}" ) ")" ) ")" ))))); registrationlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "g" be ($#m1_subset_1 :::"ClosureOperator":::) "of" (Set (Const "A")); cluster (Set ($#k10_closure2 :::"ClOp->ClSys"::: ) "g") -> ($#v11_closure2 :::"strict"::: ) ($#v15_closure2 :::"absolutely-multiplicative"::: ) ; end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Const "S")); let "C" be ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "A"))); func :::"Cl"::: "C" -> ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A")) means :: CLOSURE2:def 22 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") "st" (Bool "(" (Bool it ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) ))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A")) : (Bool "(" (Bool "C" ($#r2_pboole :::"c='"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_closure2 :::"Family"::: ) "of" "A")) ")" ) "}" ) ")" )); end; :: deftheorem defines :::"Cl"::: CLOSURE2:def 22 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_closure2 :::"Cl"::: ) (Set (Var "C")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r6_pboole :::"="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) ))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) : (Bool "(" (Bool (Set (Var "C")) ($#r2_pboole :::"c='"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "A")))) ")" ) "}" ) ")" )) ")" ))))); theorem :: CLOSURE2:38 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "D")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set ($#k11_closure2 :::"Cl"::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k7_closure2 :::"."::: ) (Set (Var "a"))) ($#r6_pboole :::"="::: ) (Set (Var "a"))))))) ; theorem :: CLOSURE2:39 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_closure2 :::"."::: ) (Set (Var "a"))) ($#r6_pboole :::"="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set ($#k11_closure2 :::"Cl"::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "D")))))))) ; theorem :: CLOSURE2:40 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetOp":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set ($#k11_closure2 :::"Cl"::: ) (Set (Var "x")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_closure2 :::"reflexive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v8_closure2 :::"monotonic"::: ) ) & (Bool (Set (Var "f")) "is" ($#v9_closure2 :::"idempotent"::: ) ) ")" )))) ; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "D" be ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Const "S")); func :::"ClSys->ClOp"::: "D" -> ($#m1_subset_1 :::"ClosureOperator":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "D") means :: CLOSURE2:def 23 (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "D")) "holds" (Bool (Set it ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set ($#k11_closure2 :::"Cl"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"ClSys->ClOp"::: CLOSURE2:def 23 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"ClosureOperator":::) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_closure2 :::"ClSys->ClOp"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_closure2 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D")))) "holds" (Bool (Set (Set (Var "b3")) ($#k7_closure2 :::"."::: ) (Set (Var "x"))) ($#r6_pboole :::"="::: ) (Set ($#k11_closure2 :::"Cl"::: ) (Set (Var "x"))))) ")" )))); theorem :: CLOSURE2:41 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"ClosureOperator":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k12_closure2 :::"ClSys->ClOp"::: ) (Set "(" ($#k10_closure2 :::"ClOp->ClSys"::: ) (Set (Var "f")) ")" )) ($#r1_funct_2 :::"="::: ) (Set (Var "f")))))) ; theorem :: CLOSURE2:42 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "D")) "being" ($#l1_closure2 :::"ClosureSystem":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k10_closure2 :::"ClOp->ClSys"::: ) (Set "(" ($#k12_closure2 :::"ClSys->ClOp"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_closure2 :::"ClosureStr"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "D"))) "," (Set "the" ($#u1_closure2 :::"Family"::: ) "of" (Set (Var "D"))) "#)" )))) ;