:: MSSUBFAM semantic presentation begin registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I")); cluster (Set ($#k2_funct_6 :::"doms"::: ) "F") -> "I" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set ($#k3_funct_6 :::"rngs"::: ) "F") -> "I" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I")); cluster (Set ($#k2_funct_6 :::"doms"::: ) "F") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k3_funct_6 :::"rngs"::: ) "F") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; scheme :: MSSUBFAM:sch 1 MSFExFunc{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool P1[(Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "," (Set (Var "x")) "," (Set (Var "i"))]) ")" ) ")" )))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool P1[(Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "i"))]) ")" )))) proof end; theorem :: MSSUBFAM:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "sf")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "sf")))))) ; theorem :: MSSUBFAM:2 (Bool "for" (Set (Var "I")) "," (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set (Var "sf")))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))) ; theorem :: MSSUBFAM:3 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "sf")))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: MSSUBFAM:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "Z1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z1")) ($#r2_hidden :::"in"::: ) (Set (Var "sf")))) "holds" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Z1"))) ")" )) "holds" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))))))) ; theorem :: MSSUBFAM:5 (Bool "for" (Set (Var "I")) "," (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "sf")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Z1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z1")) ($#r2_hidden :::"in"::: ) (Set (Var "sf")))) "holds" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "Z1"))) ")" )) "holds" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf")))))) ; theorem :: MSSUBFAM:6 (Bool "for" (Set (Var "I")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set (Var "sf"))) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "H")))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))) ($#r1_tarski :::"c="::: ) (Set (Var "H"))))) ; theorem :: MSSUBFAM:7 (Bool "for" (Set (Var "I")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set (Var "sf"))) & (Bool (Set (Var "G")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "H")))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "H"))))) ; theorem :: MSSUBFAM:8 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sh")) "," (Set (Var "sf")) "," (Set (Var "sg")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "sh")) ($#r1_hidden :::"="::: ) (Set (Set (Var "sf")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "sg"))))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sh"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sg")) ")" ))))) ; theorem :: MSSUBFAM:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "sf")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))))) ; theorem :: MSSUBFAM:10 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "sf")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "sf")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "sf"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "w"))))))) ; theorem :: MSSUBFAM:11 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_pboole :::"Element"::: ) "of" (Set (Var "B"))))) ; theorem :: MSSUBFAM:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_pboole :::"Element"::: ) "of" (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "B")))))) ; theorem :: MSSUBFAM:13 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))))) ; theorem :: MSSUBFAM:14 (Bool "for" (Set (Var "i")) "," (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))))) ; theorem :: MSSUBFAM:15 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F"))) "is" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I"))))) ; theorem :: MSSUBFAM:16 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))) "holds" (Bool (Set (Var "F")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))))) ; theorem :: MSSUBFAM:17 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set (Var "B"))) & (Bool (Set (Var "F")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")))) "holds" (Bool "(" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F"))) ($#r2_pboole :::"c="::: ) (Set (Var "B"))) ")" )))) ; begin registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> bbbadV2_FINSET_1() for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_pboole :::"[[0]]"::: ) "I") -> bbbadV3_RELAT_1() bbbadV2_FINSET_1() ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV2_FINSET_1() for ($#m3_pboole :::"ManySortedSubset"::: ) "of" "A"; end; theorem :: MSSUBFAM:18 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" bbbadV2_FINSET_1())) "holds" (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1()))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster -> bbbadV2_FINSET_1() for ($#m3_pboole :::"ManySortedSubset"::: ) "of" "A"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "A" ($#k2_pboole :::"\/"::: ) "B") -> bbbadV2_FINSET_1() ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "B" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "A" ($#k3_pboole :::"/\"::: ) "B") -> bbbadV2_FINSET_1() ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "A" ($#k3_pboole :::"/\"::: ) "B") -> bbbadV2_FINSET_1() ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "A" ($#k4_pboole :::"\"::: ) "B") -> bbbadV2_FINSET_1() ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "I")); let "A" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "F" ($#k9_pboole :::".:.:"::: ) "A") -> bbbadV2_FINSET_1() ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k6_pboole :::"[|"::: ) "A" "," "B" ($#k6_pboole :::"|]"::: ) ) -> bbbadV2_FINSET_1() ; end; theorem :: MSSUBFAM:19 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_RELAT_1()) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ) "is" bbbadV2_FINSET_1())) "holds" (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1()))) ; theorem :: MSSUBFAM:20 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) "is" bbbadV2_RELAT_1()) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ) "is" bbbadV2_FINSET_1())) "holds" (Bool (Set (Var "B")) "is" bbbadV2_FINSET_1()))) ; theorem :: MSSUBFAM:21 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1()) "iff" (Bool (Set ($#k1_mboolean :::"bool"::: ) (Set (Var "A"))) "is" bbbadV2_FINSET_1()) ")" ))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k1_mboolean :::"bool"::: ) "M") -> bbbadV2_FINSET_1() ; end; theorem :: MSSUBFAM:22 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1()) & (Bool "(" "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "M")) ($#r1_pboole :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "M")) "is" bbbadV2_FINSET_1()) ")" )) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set (Var "A"))) "is" bbbadV2_FINSET_1()))) ; theorem :: MSSUBFAM:23 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_mboolean :::"union"::: ) (Set (Var "A"))) "is" bbbadV2_FINSET_1())) "holds" (Bool "(" (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1()) & (Bool "(" "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "M")) ($#r1_pboole :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "M")) "is" bbbadV2_FINSET_1()) ")" ) ")" ))) ; theorem :: MSSUBFAM:24 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F"))) "is" bbbadV2_FINSET_1())) "holds" (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F"))) "is" bbbadV2_FINSET_1()))) ; theorem :: MSSUBFAM:25 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F")))) & (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 (Var "I"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )) "holds" (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1())))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k7_pboole :::"(Funcs)"::: ) "(" "A" "," "B" ")" ) -> bbbadV2_FINSET_1() ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "A" ($#k5_pboole :::"\+\"::: ) "B") -> bbbadV2_FINSET_1() ; end; theorem :: MSSUBFAM:26 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) "is" bbbadV2_FINSET_1()) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1()) & (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "B")) "is" bbbadV2_FINSET_1()) & (Bool (Set (Var "B")) ($#r2_pboole :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )) ")" )))) ; theorem :: MSSUBFAM:27 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) "is" bbbadV2_FINSET_1()) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "A")) "is" bbbadV2_FINSET_1()) & (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) )) ")" )))) ; theorem :: MSSUBFAM:28 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" bbbadV2_RELAT_1() bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool (Bool "not" (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "B")) ($#r2_pboole :::"c="::: ) (Set (Var "A"))) ")" )) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool "(" "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "K")) ($#r1_pboole :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Var "m")) ($#r2_pboole :::"c="::: ) (Set (Var "K"))) ")" ) ")" )))) ; theorem :: MSSUBFAM:29 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" bbbadV2_RELAT_1() bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool (Bool "not" (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "B")) ($#r2_pboole :::"c="::: ) (Set (Var "A"))) ")" )) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool "(" "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "K")) ($#r1_pboole :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Var "K")) ($#r2_pboole :::"c="::: ) (Set (Var "m"))) ")" ) ")" )))) ; theorem :: MSSUBFAM:30 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "Z")) "is" bbbadV2_FINSET_1()) & (Bool (Set (Var "Z")) ($#r2_pboole :::"c="::: ) (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_pboole :::"c="::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F")))) & (Bool (Set (Var "Y")) "is" bbbadV2_FINSET_1()) & (Bool (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set (Var "Z"))) ")" ))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode MSSubsetFamily of "M" is ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"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" -> ($#m3_pboole :::"MSSubsetFamily":::) "of" "M"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV2_FINSET_1() for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; theorem :: MSSUBFAM:31 (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 ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))) "is" bbbadV3_RELAT_1() bbbadV2_FINSET_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M"))))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV2_FINSET_1() for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "SF" be ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Const "M")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); :: original: :::"."::: redefine func "SF" :::"."::: "i" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" "M" ($#k1_funct_1 :::"."::: ) "i" ")" ); end; theorem :: MSSUBFAM:32 (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 "SF")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "SF")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))) ; theorem :: MSSUBFAM:33 (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 "SF")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "SF")))) "holds" (Bool (Set (Var "A")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")))))) ; theorem :: MSSUBFAM: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 "SF")) "," (Set (Var "SG")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k2_pboole :::"\/"::: ) (Set (Var "SG"))) "is" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: MSSUBFAM: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 "SF")) "," (Set (Var "SG")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k3_pboole :::"/\"::: ) (Set (Var "SG"))) "is" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: MSSUBFAM:36 (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 "SF")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k4_pboole :::"\"::: ) (Set (Var "A"))) "is" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: MSSUBFAM: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 "SF")) "," (Set (Var "SG")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "SF")) ($#k5_pboole :::"\+\"::: ) (Set (Var "SG"))) "is" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")))))) ; theorem :: MSSUBFAM:38 (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_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ) "is" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M"))))) ; theorem :: MSSUBFAM:39 (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_pzfmisc1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_pzfmisc1 :::"}"::: ) ) "is" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M"))))) ; theorem :: MSSUBFAM:40 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set (Var "SF"))) ($#r2_pboole :::"c="::: ) (Set (Var "M")))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "SF" be ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Const "M")); func :::"meet"::: "SF" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: MSSUBFAM:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" "M" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set "SF" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "Q")))) ")" ))); end; :: deftheorem defines :::"meet"::: MSSUBFAM: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 "SF")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_mssubfam :::"meet"::: ) (Set (Var "SF")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "SF")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "Q")))) ")" ))) ")" ))))); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "SF" be ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Const "M")); :: original: :::"meet"::: redefine func :::"meet"::: "SF" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M"; end; theorem :: MSSUBFAM:41 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "SF")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))) ($#r6_pboole :::"="::: ) (Set (Var "M")))))) ; theorem :: MSSUBFAM:42 (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 "SFe")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SFe"))) ($#r2_pboole :::"c="::: ) (Set ($#k2_mboolean :::"union"::: ) (Set (Var "SFe"))))))) ; theorem :: MSSUBFAM:43 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "SF")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))) ($#r2_pboole :::"c="::: ) (Set (Var "A")))))) ; theorem :: MSSUBFAM:44 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))) ($#r1_pboole :::"in"::: ) (Set (Var "SF")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))))) ; theorem :: MSSUBFAM:45 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "," (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "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")) ($#r1_pboole :::"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 (Var "SF"))))))) ; theorem :: MSSUBFAM:46 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "SF")) ($#r2_pboole :::"c="::: ) (Set (Var "SG")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SG"))) ($#r2_pboole :::"c="::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))))) ; theorem :: MSSUBFAM:47 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) & (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))) ($#r2_pboole :::"c="::: ) (Set (Var "B")))))) ; theorem :: MSSUBFAM:48 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "SF"))) & (Bool (Set (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF")) ")" ) ($#k3_pboole :::"/\"::: ) (Set (Var "B"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))))) ; theorem :: MSSUBFAM:49 (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 "SH")) "," (Set (Var "SF")) "," (Set (Var "SG")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "SH")) ($#r6_pboole :::"="::: ) (Set (Set (Var "SF")) ($#k2_pboole :::"\/"::: ) (Set (Var "SG"))))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SH"))) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF")) ")" ) ($#k3_pboole :::"/\"::: ) (Set "(" ($#k4_mssubfam :::"meet"::: ) (Set (Var "SG")) ")" )))))) ; theorem :: MSSUBFAM:50 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "V")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "SF")) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "V")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))) ($#r6_pboole :::"="::: ) (Set (Var "V"))))))) ; theorem :: MSSUBFAM:51 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "SF")) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "V")) "," (Set (Var "W")) ($#k2_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "V")) ($#k3_pboole :::"/\"::: ) (Set (Var "W")))))))) ; theorem :: MSSUBFAM:52 (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set (Var "SF")))) "holds" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "B"))))))) ; theorem :: MSSUBFAM:53 (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 "SF")) "being" bbbadV2_RELAT_1() ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "M"))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set (Var "SF")))) "holds" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "SF"))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "IT" be ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Const "M")); attr "IT" is :::"additive"::: means :: MSSUBFAM:def 2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "I" "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) "IT") & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) "IT")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "B"))) ($#r1_pboole :::"in"::: ) "IT")); attr "IT" is :::"absolutely-additive"::: means :: MSSUBFAM:def 3 (Bool "for" (Set (Var "F")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" "M" "st" (Bool (Bool (Set (Var "F")) ($#r2_pboole :::"c="::: ) "IT")) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set (Var "F"))) ($#r1_pboole :::"in"::: ) "IT")); attr "IT" is :::"multiplicative"::: means :: MSSUBFAM:def 4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "I" "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) "IT") & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) "IT")) "holds" (Bool (Set (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B"))) ($#r1_pboole :::"in"::: ) "IT")); attr "IT" is :::"absolutely-multiplicative"::: means :: MSSUBFAM:def 5 (Bool "for" (Set (Var "F")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" "M" "st" (Bool (Bool (Set (Var "F")) ($#r2_pboole :::"c="::: ) "IT")) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "F"))) ($#r1_pboole :::"in"::: ) "IT")); attr "IT" is :::"properly-upper-bound"::: means :: MSSUBFAM:def 6 (Bool "M" ($#r1_pboole :::"in"::: ) "IT"); attr "IT" is :::"properly-lower-bound"::: means :: MSSUBFAM:def 7 (Bool (Set ($#k1_pboole :::"[[0]]"::: ) "I") ($#r1_pboole :::"in"::: ) "IT"); end; :: deftheorem defines :::"additive"::: MSSUBFAM:def 2 : (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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_mssubfam :::"additive"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "B"))) ($#r1_pboole :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"absolutely-additive"::: MSSUBFAM: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 "IT")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_mssubfam :::"absolutely-additive"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "F")) ($#r2_pboole :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set (Var "F"))) ($#r1_pboole :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"multiplicative"::: MSSUBFAM: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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_mssubfam :::"multiplicative"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "B")) ($#r1_pboole :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B"))) ($#r1_pboole :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"absolutely-multiplicative"::: MSSUBFAM: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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "F")) ($#r2_pboole :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set (Var "F"))) ($#r1_pboole :::"in"::: ) (Set (Var "IT")))) ")" )))); :: deftheorem defines :::"properly-upper-bound"::: MSSUBFAM: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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_mssubfam :::"properly-upper-bound"::: ) ) "iff" (Bool (Set (Var "M")) ($#r1_pboole :::"in"::: ) (Set (Var "IT"))) ")" )))); :: deftheorem defines :::"properly-lower-bound"::: MSSUBFAM: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" ($#m3_pboole :::"MSSubsetFamily":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_mssubfam :::"properly-lower-bound"::: ) ) "iff" (Bool (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))) ($#r1_pboole :::"in"::: ) (Set (Var "IT"))) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_mssubfam :::"additive"::: ) ($#v2_mssubfam :::"absolutely-additive"::: ) ($#v3_mssubfam :::"multiplicative"::: ) ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#v6_mssubfam :::"properly-lower-bound"::: ) for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"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_mssubfam :::"additive"::: ) ($#v2_mssubfam :::"absolutely-additive"::: ) ($#v3_mssubfam :::"multiplicative"::: ) ($#v4_mssubfam :::"absolutely-multiplicative"::: ) ($#v5_mssubfam :::"properly-upper-bound"::: ) ($#v6_mssubfam :::"properly-lower-bound"::: ) ($#m3_pboole :::"MSSubsetFamily":::) "of" "M"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v2_mssubfam :::"absolutely-additive"::: ) -> ($#v1_mssubfam :::"additive"::: ) for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v4_mssubfam :::"absolutely-multiplicative"::: ) -> ($#v3_mssubfam :::"multiplicative"::: ) for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v4_mssubfam :::"absolutely-multiplicative"::: ) -> ($#v5_mssubfam :::"properly-upper-bound"::: ) for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v5_mssubfam :::"properly-upper-bound"::: ) -> bbbadV2_RELAT_1() for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v2_mssubfam :::"absolutely-additive"::: ) -> ($#v6_mssubfam :::"properly-lower-bound"::: ) for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v6_mssubfam :::"properly-lower-bound"::: ) -> bbbadV2_RELAT_1() for ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k1_mboolean :::"bool"::: ) "M"); end;