:: ARYTM_0 semantic presentation begin theorem :: ARYTM_0:1 (Bool (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: ARYTM_0:2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: ARYTM_0:3 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) ; theorem :: ARYTM_0:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: ARYTM_0:5 (Bool (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ; begin theorem :: ARYTM_0:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: ARYTM_0:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )) & (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; begin definitionlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"+"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: ARYTM_0:def 1 (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool "y" ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")))) ")" )) if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "y9")))) ")" )) if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool "y" ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "x9")))) ")" )) if (Bool "(" (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) otherwise (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")))) ")" )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "y9")))) ")" )) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "x9")))) ")" )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")))) ")" )) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "y9")))) ")" )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "x9")))) ")" )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" ")" )) ; func :::"*"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: ARYTM_0:def 2 (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool "y" ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")))) ")" )) if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "x" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool "y" ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) if (Bool "(" (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "y" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")))) ")" )) if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")))) ")" )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")))) ")" )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")))) ")" )) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")))) ")" )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ; end; :: deftheorem defines :::"+"::: ARYTM_0:def 1 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "y9")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k2_arytm_1 :::"-"::: ) (Set (Var "x9")))) ")" )) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" ) ")" ")" )); :: deftheorem defines :::"*"::: ARYTM_0:def 2 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y9")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "x9")))) ")" )) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" )); definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"opp"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: ARYTM_0:def 3 (Bool (Set ($#k1_arytm_0 :::"+"::: ) "(" "x" "," it ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "b2")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; func :::"inv"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: ARYTM_0:def 4 (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" "x" "," it ")" ) ($#r1_hidden :::"="::: ) (Num 1)) if (Bool "x" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Bool (Set (Var "b2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "b2")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "b2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "b1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ; end; :: deftheorem defines :::"opp"::: ARYTM_0:def 3 : (Bool "for" (Set (Var "x")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_arytm_0 :::"opp"::: ) (Set (Var "x")))) "iff" (Bool (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); :: deftheorem defines :::"inv"::: ARYTM_0:def 4 : (Bool "for" (Set (Var "x")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_0 :::"inv"::: ) (Set (Var "x")))) "iff" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_0 :::"inv"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" )); begin theorem :: ARYTM_0:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Bool "not" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; definitionlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"[*":::"x" "," "y":::"*]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: ARYTM_0:def 5 "x" if (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k5_funct_4 :::"-->"::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"[*"::: ARYTM_0:def 5 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k5_arytm_0 :::"*]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k5_arytm_0 :::"*]"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ")" )); theorem :: ARYTM_0:9 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "ex" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k5_arytm_0 :::"*]"::: ) )))) ; theorem :: ARYTM_0:10 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_arytm_0 :::"*]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k5_arytm_0 :::"*]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" )) ; theorem :: ARYTM_0:11 (Bool "for" (Set (Var "x")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: ARYTM_0:12 (Bool "for" (Set (Var "x")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ARYTM_0:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set (Var "z")) ")" ))) ; theorem :: ARYTM_0:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ")" ) ")" ))) ; theorem :: ARYTM_0:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set "(" ($#k3_arytm_0 :::"opp"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_arytm_0 :::"opp"::: ) (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))) ; theorem :: ARYTM_0:16 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) ))) ; theorem :: ARYTM_0:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ")" ) "," (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "y")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ARYTM_0:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: ARYTM_0:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: ARYTM_0:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set "(" ($#k4_arytm_0 :::"inv"::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: ARYTM_0:21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "not" (Bool (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: ARYTM_0:22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_arytm_0 :::"inv"::: ) (Set "(" ($#k2_arytm_0 :::"*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_arytm_0 :::"*"::: ) "(" (Set "(" ($#k4_arytm_0 :::"inv"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k4_arytm_0 :::"inv"::: ) (Set (Var "y")) ")" ) ")" ))) ; theorem :: ARYTM_0:23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set "(" ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set (Var "z")) ")" ))) ; theorem :: ARYTM_0:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k5_arytm_0 :::"*]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ARYTM_0:25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k3_arytm_0 :::"opp"::: ) (Set "(" ($#k1_arytm_0 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_arytm_0 :::"+"::: ) "(" (Set "(" ($#k3_arytm_0 :::"opp"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k3_arytm_0 :::"opp"::: ) (Set (Var "y")) ")" ) ")" ))) ;