:: PZFMISC1 semantic presentation begin theorem :: PZFMISC1:1 (Bool "for" (Set (Var "I")) "," (Set (Var "i")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "i")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "I"))))) ; theorem :: PZFMISC1:2 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "f")) "is" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PZFMISC1:3 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" "not" (Bool (Set (Var "X")) "is" bbbadV3_RELAT_1()) "or" "not" (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1()) ")" ))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"{":::"A":::"}"::: -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PZFMISC1:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_tarski :::"}"::: ) ))); end; :: deftheorem defines :::"{"::: PZFMISC1:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) )) "iff" (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 (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_tarski :::"}"::: ) ))) ")" ))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k1_pzfmisc1 :::"{"::: ) "A" ($#k1_pzfmisc1 :::"}"::: ) ) -> bbbadV2_RELAT_1() bbbadV2_FINSET_1() ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"{":::"A" "," "B":::"}"::: -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PZFMISC1:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) ))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) )))) ; end; :: deftheorem defines :::"{"::: PZFMISC1:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_pzfmisc1 :::"}"::: ) )) "iff" (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 (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_tarski :::"}"::: ) ))) ")" ))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set ($#k2_pzfmisc1 :::"{"::: ) "A" "," "B" ($#k2_pzfmisc1 :::"}"::: ) ) -> bbbadV2_RELAT_1() bbbadV2_FINSET_1() ; end; theorem :: PZFMISC1:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "y"))) ")" )) ")" ))) ; theorem :: PZFMISC1:5 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "x2"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_pzfmisc1 :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "x2"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))))) ; theorem :: PZFMISC1:7 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "A"))))) ; theorem :: PZFMISC1:8 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:10 (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")) "holds" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "B")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:11 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:12 (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 ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "B")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set (Var "B"))))) ; theorem :: PZFMISC1:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "y"))))) ; theorem :: PZFMISC1:14 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_pzfmisc1 :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "B"))) ")" ))) ; theorem :: PZFMISC1:15 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set (Var "B"))))) ; theorem :: PZFMISC1:16 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) & (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ")" ))) ; theorem :: PZFMISC1:17 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) "or" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "y"))))) ; theorem :: PZFMISC1:18 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:19 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))))) ; theorem :: PZFMISC1:20 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) "or" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "y"))))) ; theorem :: PZFMISC1:21 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) & (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ")" ))) ; theorem :: PZFMISC1:22 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))))) ; theorem :: PZFMISC1:23 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "y"))))) ; theorem :: PZFMISC1:24 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) & (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) ")" ))) ; theorem :: PZFMISC1:25 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:26 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r6_pboole :::"="::: ) (Set (Var "A"))) ")" ))) ; theorem :: PZFMISC1:27 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:28 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k1_mboolean :::"bool"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set "(" ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")) ")" ) "," (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1: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 ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k1_mboolean :::"bool"::: ) (Set (Var "A")))))) ; theorem :: PZFMISC1:30 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set (Var "x"))))) ; theorem :: PZFMISC1:31 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) "," (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:32 (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")) "holds" (Bool (Set ($#k2_mboolean :::"union"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "B")))))) ; theorem :: PZFMISC1:33 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) ")" ))) ; theorem :: PZFMISC1:34 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x2")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) ")" ) ")" ))) ; theorem :: PZFMISC1:35 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "or" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x1")) ($#k1_pzfmisc1 :::"}"::: ) )) "or" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x2")) ($#k1_pzfmisc1 :::"}"::: ) )) "or" (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_pzfmisc1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_pzfmisc1 :::"}"::: ) )))) ; begin theorem :: PZFMISC1:36 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "A"))) "or" (Bool (Set (Var "x")) ($#r6_pboole :::"="::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "B")) ($#k1_pzfmisc1 :::"}"::: ) ))))) ; theorem :: PZFMISC1:37 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r2_pboole :::"c="::: ) (Set (Var "B"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B"))) ")" ) ")" ))) ; theorem :: PZFMISC1:38 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))))) ; theorem :: PZFMISC1:39 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set (Var "X"))))) ; theorem :: PZFMISC1:40 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set (Var "A"))) ($#r6_pboole :::"="::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Var "A"))) ")" ) ")" ))) ; theorem :: PZFMISC1:41 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PZFMISC1:42 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k2_pboole :::"\/"::: ) (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; begin theorem :: PZFMISC1:43 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))))) ; theorem :: PZFMISC1:44 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )))) ; theorem :: PZFMISC1:45 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) ")" ) "iff" (Bool (Set (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ")" ))) ; theorem :: PZFMISC1:46 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))))) ; theorem :: PZFMISC1:47 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k3_pboole :::"/\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) ")" ))) ; begin theorem :: PZFMISC1:48 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )))) "holds" (Bool (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))))) ; theorem :: PZFMISC1:49 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))))) ; theorem :: PZFMISC1:50 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set (Var "X")))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))))) ; theorem :: PZFMISC1:51 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))))) ; theorem :: PZFMISC1:52 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "iff" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) ")" ))) ; theorem :: PZFMISC1:53 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))))) ; theorem :: PZFMISC1:54 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "I")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Var "X")))) ")" ))) ; theorem :: PZFMISC1:55 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k4_pboole :::"\"::: ) (Set (Var "X"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_pboole :::"in"::: ) (Set (Var "X"))) ")" ) ")" ))) ; theorem :: PZFMISC1:56 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "or" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) )) "or" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) )) "or" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; begin theorem :: PZFMISC1:57 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "or" (Bool (Set (Var "Y")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) ")" )) "holds" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PZFMISC1:58 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1()) & (Bool (Set (Var "Y")) "is" bbbadV2_RELAT_1()) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Var "Y"))))) ; theorem :: PZFMISC1:59 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set (Var "Y"))))) ; theorem :: PZFMISC1:60 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "Z")) "is" bbbadV2_RELAT_1()) & (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) )) "or" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))))) ; theorem :: PZFMISC1:61 (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")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) )) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) )) ")" ))) ; theorem :: PZFMISC1:62 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "A")) "," (Set (Var "x2")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_pboole :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_pboole :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )))) ; theorem :: PZFMISC1:63 (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")) "holds" (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ))) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set "(" (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ))) ")" ))) ; theorem :: PZFMISC1:64 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "x1")) ($#k2_pboole :::"\/"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "B")) ")" ) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set (Var "A")) ($#k6_pboole :::"|]"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ) ")" ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x2")) "," (Set (Var "A")) ($#k6_pboole :::"|]"::: ) ) ")" ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x2")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ))))) ; theorem :: PZFMISC1:65 (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")) "holds" (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ))) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set "(" (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ))) ")" ))) ; theorem :: PZFMISC1:66 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "x1")) ($#k3_pboole :::"/\"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B")) ")" ) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set (Var "A")) ($#k6_pboole :::"|]"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x2")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ))))) ; theorem :: PZFMISC1:67 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "B")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "B")) ($#r2_pboole :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )))) ; theorem :: PZFMISC1:68 (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")) "holds" (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ) ($#k4_pboole :::"\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k6_pboole :::"|]"::: ) ))) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set "(" (Set (Var "X")) ($#k4_pboole :::"\"::: ) (Set (Var "Y")) ")" ) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#k4_pboole :::"\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ))) ")" ))) ; theorem :: PZFMISC1:69 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k6_pboole :::"|]"::: ) ) ($#k4_pboole :::"\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "x1")) ($#k4_pboole :::"\"::: ) (Set (Var "A")) ")" ) "," (Set (Var "x2")) ($#k6_pboole :::"|]"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set "(" (Set (Var "x2")) ($#k4_pboole :::"\"::: ) (Set (Var "B")) ")" ) ($#k6_pboole :::"|]"::: ) ))))) ; theorem :: PZFMISC1:70 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "x1")) ($#k3_pboole :::"/\"::: ) (Set (Var "x2"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) "or" (Bool (Set (Set (Var "A")) ($#k3_pboole :::"/\"::: ) (Set (Var "B"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))) ")" )) "holds" (Bool (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set (Var "A")) ($#k6_pboole :::"|]"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x2")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PZFMISC1:71 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "X")) "is" bbbadV2_RELAT_1())) "holds" (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) "is" bbbadV2_RELAT_1()) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k6_pboole :::"|]"::: ) ) "is" bbbadV2_RELAT_1()) ")" ))) ; theorem :: PZFMISC1:72 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ))) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set ($#k2_pzfmisc1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_pzfmisc1 :::"}"::: ) ) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "x")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k6_pboole :::"|]"::: ) ) ($#k2_pboole :::"\/"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "y")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k6_pboole :::"|]"::: ) ))) ")" ))) ; theorem :: PZFMISC1:73 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "A")) "," (Set (Var "x2")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x1")) "is" bbbadV2_RELAT_1()) & (Bool (Set (Var "A")) "is" bbbadV2_RELAT_1()) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x1")) "," (Set (Var "A")) ($#k6_pboole :::"|]"::: ) ) ($#r6_pboole :::"="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x2")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r6_pboole :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "A")) ($#r6_pboole :::"="::: ) (Set (Var "B"))) ")" ))) ; theorem :: PZFMISC1:74 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) )) "or" (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PZFMISC1:75 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k6_pboole :::"|]"::: ) )) & (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_pboole :::"in"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "x")) ($#k3_pboole :::"/\"::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set (Var "y")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k6_pboole :::"|]"::: ) )))) ; theorem :: PZFMISC1:76 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "y")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) )) & (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "x")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) ) "is" bbbadV2_RELAT_1())) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_pboole :::"c="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: PZFMISC1:77 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) )))) ; theorem :: PZFMISC1:78 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ) ($#k3_pboole :::"/\"::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) )) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I")))))) ; theorem :: PZFMISC1:79 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "A")) "is" bbbadV2_RELAT_1()) & (Bool "(" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) )) "or" (Bool (Set ($#k6_pboole :::"[|"::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k6_pboole :::"|]"::: ) ) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k6_pboole :::"|]"::: ) )) ")" )) "holds" (Bool (Set (Var "B")) ($#r2_pboole :::"c="::: ) (Set (Var "Y"))))) ; theorem :: PZFMISC1:80 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )) & (Bool (Set (Var "y")) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k2_pboole :::"\/"::: ) (Set (Var "y"))) ($#r2_pboole :::"c="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set (Var "B")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y")) ")" ) ($#k6_pboole :::"|]"::: ) )))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); pred "A" :::"is_transformable_to"::: "B" means :: PZFMISC1:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I") & (Bool (Set "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); reflexivity (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Const "I"))) & (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; end; :: deftheorem defines :::"is_transformable_to"::: PZFMISC1:def 3 : (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")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_pzfmisc1 :::"is_transformable_to"::: ) (Set (Var "B"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )));