:: MCART_1 semantic presentation begin theorem :: MCART_1:1 canceled; theorem :: MCART_1:2 canceled; theorem :: MCART_1:3 canceled; theorem :: MCART_1:4 canceled; theorem :: MCART_1:5 canceled; theorem :: MCART_1:6 canceled; theorem :: MCART_1:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: MCART_1:8 (Bool "for" (Set (Var "p")) "being" ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "p")))) ; theorem :: MCART_1:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ) "or" "not" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ) ")" ))) ; theorem :: MCART_1:10 (Bool "for" (Set (Var "z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ; theorem :: MCART_1:11 (Bool "for" (Set (Var "z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: MCART_1:12 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ; theorem :: MCART_1:13 (Bool "for" (Set (Var "z")) "," (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: MCART_1:14 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: MCART_1:15 (Bool "for" (Set (Var "z")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ; theorem :: MCART_1:16 (Bool "for" (Set (Var "z")) "," (Set (Var "X")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) "or" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" ) ")" )) ; theorem :: MCART_1:17 (Bool "for" (Set (Var "z")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: MCART_1:18 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "(" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) "or" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" ) ")" )) ; theorem :: MCART_1:19 (Bool "for" (Set (Var "z")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) "or" (Bool (Set (Set (Var "z")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ) & (Bool "(" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) "or" (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" ) ")" )) ; theorem :: MCART_1:20 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" )) ; theorem :: MCART_1:21 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )))) ; theorem :: MCART_1:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )))) ; theorem :: MCART_1:23 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: MCART_1:24 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" ))) ; theorem :: MCART_1:25 canceled; theorem :: MCART_1:26 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ) "or" "not" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) )) ")" ) ")" ) ")" ))) ; theorem :: MCART_1:27 canceled; theorem :: MCART_1:28 canceled; theorem :: MCART_1:29 canceled; theorem :: MCART_1:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Bool "not" (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ) "or" "not" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )) ")" ) ")" ) ")" ))) ; theorem :: MCART_1:31 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X3")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "iff" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: MCART_1:32 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X3")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_hidden :::"="::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_hidden :::"="::: ) (Set (Var "Y3"))) ")" )) ; theorem :: MCART_1:33 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_hidden :::"="::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_hidden :::"="::: ) (Set (Var "Y3"))) ")" )) ; theorem :: MCART_1:34 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) "," (Set (Var "X")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y")) "," (Set (Var "Y")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) ; theorem :: MCART_1:35 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x3")) ($#k1_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MCART_1:36 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x3")) ($#k1_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MCART_1:37 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x3")) ($#k1_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MCART_1:38 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x3")) "," (Set (Var "y3")) ($#k2_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MCART_1:39 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x3")) ($#k1_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: MCART_1:40 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x3")) "," (Set (Var "y3")) ($#k2_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: MCART_1:41 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x3")) "," (Set (Var "y3")) ($#k2_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: MCART_1:42 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x3")) "," (Set (Var "y3")) ($#k2_tarski :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k6_enumset1 :::"}"::: ) ))) ; registrationlet "X1", "X2", "X3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_xtuple_0 :::"triple"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" ($#k3_zfmisc_1 :::":]"::: ) ); end; definitioncanceled; canceled; canceled; canceled; let "X1", "X2", "X3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Const "X1")) "," (Set (Const "X2")) "," (Set (Const "X3")) ($#k3_zfmisc_1 :::":]"::: ) ); :: original: :::"`1_3"::: redefine func "x" :::"`1_3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X1" means :: MCART_1:def 5 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "x1")))); :: original: :::"`2_3"::: redefine func "x" :::"`2_3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X2" means :: MCART_1:def 6 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "x2")))); :: original: :::"`2"::: redefine func "x" :::"`3_3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X3" means :: MCART_1:def 7 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "x3")))); end; :: deftheorem MCART_1:def 1 : canceled; :: deftheorem MCART_1:def 2 : canceled; :: deftheorem MCART_1:def 3 : canceled; :: deftheorem MCART_1:def 4 : canceled; :: deftheorem defines :::"`1_3"::: MCART_1:def 5 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) ")" )))); :: deftheorem defines :::"`2_3"::: MCART_1:def 6 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) ")" )))); :: deftheorem defines :::"`3_3"::: MCART_1:def 7 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Var "x3")))) ")" )))); theorem :: MCART_1:43 canceled; theorem :: MCART_1:44 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k3_xtuple_0 :::"]"::: ) )))) ; theorem :: MCART_1:45 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#k3_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) ($#k3_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_zfmisc_1 :::":]"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: MCART_1:46 canceled; theorem :: MCART_1:47 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) )) ")" ))) ; theorem :: MCART_1:48 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y3"))) ")" )) ; theorem :: MCART_1:49 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X3")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X4")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: MCART_1:50 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ))) ; theorem :: MCART_1:51 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X3")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X4")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "iff" (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: MCART_1:52 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X3")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X4")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_hidden :::"="::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_hidden :::"="::: ) (Set (Var "Y3"))) & (Bool (Set (Var "X4")) ($#r1_hidden :::"="::: ) (Set (Var "Y4"))) ")" )) ; theorem :: MCART_1:53 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_hidden :::"="::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_hidden :::"="::: ) (Set (Var "Y3"))) & (Bool (Set (Var "X4")) ($#r1_hidden :::"="::: ) (Set (Var "Y4"))) ")" )) ; theorem :: MCART_1:54 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) "," (Set (Var "X")) "," (Set (Var "X")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y")) "," (Set (Var "Y")) "," (Set (Var "Y")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) ; registrationlet "X1", "X2", "X3", "X4" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_xtuple_0 :::"quadruple"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" "," "X4" ($#k4_zfmisc_1 :::":]"::: ) ); end; definitionlet "X1", "X2", "X3", "X4" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Const "X1")) "," (Set (Const "X2")) "," (Set (Const "X3")) "," (Set (Const "X4")) ($#k4_zfmisc_1 :::":]"::: ) ); :: original: :::"`1_4"::: redefine func "x" :::"`1_4"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X1" means :: MCART_1:def 8 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "x1")))); :: original: :::"`2_4"::: redefine func "x" :::"`2_4"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X2" means :: MCART_1:def 9 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "x2")))); :: original: :::"`2_3"::: redefine func "x" :::"`3_4"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X3" means :: MCART_1:def 10 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "x3")))); :: original: :::"`2"::: redefine func "x" :::"`4_4"::: -> ($#m1_subset_1 :::"Element"::: ) "of" "X4" means :: MCART_1:def 11 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "x4")))); end; :: deftheorem defines :::"`1_4"::: MCART_1:def 8 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) ")" )))); :: deftheorem defines :::"`2_4"::: MCART_1:def 9 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) ")" )))); :: deftheorem defines :::"`3_4"::: MCART_1:def 10 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Var "x3")))) ")" )))); :: deftheorem defines :::"`4_4"::: MCART_1:def 11 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Var "x4")))) ")" )))); theorem :: MCART_1:55 canceled; theorem :: MCART_1:56 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) ")" ) ($#k6_xtuple_0 :::"]"::: ) )))) ; theorem :: MCART_1:57 canceled; theorem :: MCART_1:58 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) )) ")" ))) ; theorem :: MCART_1:59 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "," (Set (Var "X1")) ($#k4_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X3")) "," (Set (Var "X4")) "," (Set (Var "X1")) "," (Set (Var "X2")) ($#k4_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X4")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k4_zfmisc_1 :::":]"::: ) )) ")" )) "holds" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: MCART_1:60 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y3"))) & (Bool (Set (Var "X4")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y4"))) ")" )) ; theorem :: MCART_1:61 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x3")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x4")) ($#k1_tarski :::"}"::: ) ) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MCART_1:62 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" ))) ; theorem :: MCART_1:63 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) )) ")" )) ; theorem :: MCART_1:64 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) ")" )))) ; theorem :: MCART_1:65 (Bool "for" (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "xx1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "xx2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "xx3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "xx1")) "," (Set (Var "xx2")) "," (Set (Var "xx3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "xx1"))))) ")" )) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ))))) ; theorem :: MCART_1:66 (Bool "for" (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "xx1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "xx2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "xx3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "xx1")) "," (Set (Var "xx2")) "," (Set (Var "xx3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "y2")) ($#r1_hidden :::"="::: ) (Set (Var "xx2"))))) ")" )) "holds" (Bool (Set (Var "y2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ))))) ; theorem :: MCART_1:67 (Bool "for" (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "xx1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "xx2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "xx3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "xx1")) "," (Set (Var "xx2")) "," (Set (Var "xx3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "y3")) ($#r1_hidden :::"="::: ) (Set (Var "xx3"))))) ")" )) "holds" (Bool (Set (Var "y3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ))))) ; theorem :: MCART_1:68 (Bool "for" (Set (Var "z")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "X3"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) )) ")" ))) ; theorem :: MCART_1:69 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) )) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "X3"))) ")" ) ")" )) ; theorem :: MCART_1:70 (Bool "for" (Set (Var "Z")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "X3"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) )) ")" )) ")" ) ")" )) "holds" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ))) ; theorem :: MCART_1:71 canceled; theorem :: MCART_1:72 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) (Bool "for" (Set (Var "A3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X3")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A3"))) ")" )))))) ; theorem :: MCART_1:73 (Bool "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "," (Set (Var "X3")) "," (Set (Var "Y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_tarski :::"c="::: ) (Set (Var "Y3")))) "holds" (Bool (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) ($#k3_zfmisc_1 :::":]"::: ) ))) ; theorem :: MCART_1:74 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) & (Bool (Set (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) ")" )))) ; theorem :: MCART_1:75 (Bool "for" (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "xx1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "xx2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "xx3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "xx4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "xx1")) "," (Set (Var "xx2")) "," (Set (Var "xx3")) "," (Set (Var "xx4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "xx1")))))) ")" )) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) ))))) ; theorem :: MCART_1:76 (Bool "for" (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "xx1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "xx2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "xx3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "xx4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "xx1")) "," (Set (Var "xx2")) "," (Set (Var "xx3")) "," (Set (Var "xx4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "y2")) ($#r1_hidden :::"="::: ) (Set (Var "xx2")))))) ")" )) "holds" (Bool (Set (Var "y2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) ))))) ; theorem :: MCART_1:77 (Bool "for" (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "xx1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "xx2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "xx3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "xx4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "xx1")) "," (Set (Var "xx2")) "," (Set (Var "xx3")) "," (Set (Var "xx4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "y3")) ($#r1_hidden :::"="::: ) (Set (Var "xx3")))))) ")" )) "holds" (Bool (Set (Var "y3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) ))))) ; theorem :: MCART_1:78 (Bool "for" (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "xx1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) (Bool "for" (Set (Var "xx2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) (Bool "for" (Set (Var "xx3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X3")) (Bool "for" (Set (Var "xx4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X4")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "xx1")) "," (Set (Var "xx2")) "," (Set (Var "xx3")) "," (Set (Var "xx4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "y4")) ($#r1_hidden :::"="::: ) (Set (Var "xx4")))))) ")" )) "holds" (Bool (Set (Var "y4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) ))))) ; theorem :: MCART_1:79 (Bool "for" (Set (Var "z")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "X3"))) & (Bool (Set (Var "x4")) ($#r2_hidden :::"in"::: ) (Set (Var "X4"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )) ")" ))) ; theorem :: MCART_1:80 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) )) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "X3"))) & (Bool (Set (Var "x4")) ($#r2_hidden :::"in"::: ) (Set (Var "X4"))) ")" ) ")" )) ; theorem :: MCART_1:81 (Bool "for" (Set (Var "Z")) "," (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "X3"))) & (Bool (Set (Var "x4")) ($#r2_hidden :::"in"::: ) (Set (Var "X4"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )) ")" )) ")" ) ")" )) "holds" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ))) ; theorem :: MCART_1:82 canceled; theorem :: MCART_1:83 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) (Bool "for" (Set (Var "A3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X3")) (Bool "for" (Set (Var "A4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X4")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "A4")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_mcart_1 :::"`1_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Set (Var "x")) ($#k5_mcart_1 :::"`2_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "x")) ($#k6_mcart_1 :::"`3_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A3"))) & (Bool (Set (Set (Var "x")) ($#k7_mcart_1 :::"`4_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A4"))) ")" ))))))) ; theorem :: MCART_1:84 (Bool "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "," (Set (Var "X3")) "," (Set (Var "Y3")) "," (Set (Var "X4")) "," (Set (Var "Y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X3")) ($#r1_tarski :::"c="::: ) (Set (Var "Y3"))) & (Bool (Set (Var "X4")) ($#r1_tarski :::"c="::: ) (Set (Var "Y4")))) "holds" (Bool (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "Y3")) "," (Set (Var "Y4")) ($#k4_zfmisc_1 :::":]"::: ) ))) ; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X1")); let "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X2")); :: original: :::"[:"::: redefine func :::"[:":::"A1" "," "A2":::":]"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X1" "," "X2" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "X1", "X2", "X3" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X1")); let "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X2")); let "A3" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X3")); :: original: :::"[:"::: redefine func :::"[:":::"A1" "," "A2" "," "A3":::":]"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" ($#k3_zfmisc_1 :::":]"::: ) ); end; definitionlet "X1", "X2", "X3", "X4" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X1")); let "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X2")); let "A3" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X3")); let "A4" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X4")); :: original: :::"[:"::: redefine func :::"[:":::"A1" "," "A2" "," "A3" "," "A4":::":]"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" "," "X4" ($#k4_zfmisc_1 :::":]"::: ) ); end; begin definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"pr1"::: "f" -> ($#m1_hidden :::"Function":::) means :: MCART_1:def 12 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) ")" ) ")" ); func :::"pr2"::: "f" -> ($#m1_hidden :::"Function":::) means :: MCART_1:def 13 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"pr1"::: MCART_1:def 12 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_mcart_1 :::"pr1"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) ")" ) ")" ) ")" )); :: deftheorem defines :::"pr2"::: MCART_1:def 13 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_mcart_1 :::"pr2"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )) ")" ) ")" ) ")" )); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func "x" :::"`11"::: -> ($#m1_hidden :::"set"::: ) equals :: MCART_1:def 14 (Set (Set "(" "x" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); func "x" :::"`12"::: -> ($#m1_hidden :::"set"::: ) equals :: MCART_1:def 15 (Set (Set "(" "x" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ); func "x" :::"`21"::: -> ($#m1_hidden :::"set"::: ) equals :: MCART_1:def 16 (Set (Set "(" "x" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); func "x" :::"`22"::: -> ($#m1_hidden :::"set"::: ) equals :: MCART_1:def 17 (Set (Set "(" "x" ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ); end; :: deftheorem defines :::"`11"::: MCART_1:def 14 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k13_mcart_1 :::"`11"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))); :: deftheorem defines :::"`12"::: MCART_1:def 15 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k14_mcart_1 :::"`12"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))); :: deftheorem defines :::"`21"::: MCART_1:def 16 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k15_mcart_1 :::"`21"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))); :: deftheorem defines :::"`22"::: MCART_1:def 17 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k16_mcart_1 :::"`22"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))); theorem :: MCART_1:85 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k13_mcart_1 :::"`11"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k14_mcart_1 :::"`12"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k15_mcart_1 :::"`21"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k16_mcart_1 :::"`22"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" )) ; theorem :: MCART_1:86 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) ")" ))) ; theorem :: MCART_1:87 (Bool "for" (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "I")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "R")) : (Bool (Set (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "}" ))) ; theorem :: MCART_1:88 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" )))) ; theorem :: MCART_1:89 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: MCART_1:90 (Bool "for" (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: MCART_1:91 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: MCART_1:92 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ))) ; scheme :: MCART_1:sch 1 BiFuncEx{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))]) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))]) ")" ))) proof end;