:: ARYTM_1  semantic presentation begin  





theorem :: ARYTM_1:1 (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"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_1:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ARYTM_1:3 (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_arytm_2 :::"<='"::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "z")))) "holds"  (Bool (Set (Var "x"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "z")))) ; 
 
theorem :: ARYTM_1:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x")))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: ARYTM_1:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_1:6 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "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 (Var "x"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y")))) ; 
 
theorem :: ARYTM_1:7 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y"))) "iff" (Bool (Set (Set (Var "x"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "z")))  ($#r1_arytm_2 :::"<='"::: )  (Set (Set (Var "y"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "z"))))  ")" )) ; 
 
theorem :: ARYTM_1:8 (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_arytm_2 :::"<='"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "z")))  ($#r1_arytm_2 :::"<='"::: )  (Set (Set (Var "y"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "z"))))) ; 
 definitionlet "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ); func "x" :::"-'"::: "y" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) means :: ARYTM_1:def 1 (Bool (Set it  ($#k7_arytm_2 :::"+"::: )  "y")  ($#r1_hidden :::"="::: )  "x") if (Bool "y"  ($#r1_arytm_2 :::"<='"::: )  "x")  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )); end; 






:: deftheorem    defines :::"-'"::: ARYTM_1:def 1 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x")))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")))) "iff" (Bool (Set (Set (Var "b3"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x"))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))  ")" )  ")"   ")" )); 
 
theorem :: ARYTM_1:9 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y"))) "or" (Bool (Set (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ARYTM_1:10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y"))) & (Bool (Set (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: ARYTM_1:11 (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"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x")))) ; 
 
theorem :: ARYTM_1:12 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x"))) & (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "z")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k7_arytm_2 :::"+"::: )  (Set  "(" (Set (Var "z"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" )  ($#k7_arytm_2 :::"+"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:13 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k7_arytm_2 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "y")) ")" )  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:14 (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x"))) & (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" )  ($#k7_arytm_2 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set  "(" (Set (Var "z"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: ARYTM_1:15 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x"))) & (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "z"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" )  ($#k7_arytm_2 :::"+"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" )  ($#k7_arytm_2 :::"+"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:16 (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_arytm_2 :::"<='"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "z"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")))  ($#r1_arytm_2 :::"<='"::: )  (Set (Set (Var "z"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "x"))))) ; 
 
theorem :: ARYTM_1:17 (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_arytm_2 :::"<='"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")))  ($#r1_arytm_2 :::"<='"::: )  (Set (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z"))))) ; 
 definitionlet "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ); func "x" :::"-"::: "y" ->    ($#m1_hidden :::"set"::: )   equals :: ARYTM_1:def 2 (Set "x"  ($#k1_arytm_1 :::"-'"::: )  "y") if (Bool "y"  ($#r1_arytm_2 :::"<='"::: )  "x")  otherwise (Set  ($#k4_tarski :::"["::: ) (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set  "(" "y"  ($#k1_arytm_1 :::"-'"::: )  "x" ")" ) ($#k4_tarski :::"]"::: ) ); end; 






:: deftheorem    defines :::"-"::: ARYTM_1:def 2 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x")))) "implies" (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x"))))) "implies" (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ))  ")"   ")" )); 
 
theorem :: ARYTM_1:18 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) ; 
 
theorem :: ARYTM_1:19 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "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 (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))) ; 
 
theorem :: ARYTM_1:20 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k7_arytm_2 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "y")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:21 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Bool  "not" (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "z"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "y")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:22 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x"))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "z"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" )  ($#k7_arytm_2 :::"+"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:23 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Bool  "not" (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x")))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "z"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: ARYTM_1:24 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "y"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k7_arytm_2 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:25 (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_arytm_2 :::"<='"::: )  (Set (Var "y"))) & (Bool (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "x")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set (Var "z"))))) ; 
 
theorem :: ARYTM_1:26 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "y")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: ARYTM_1:27 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Bool  "not" (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set  "(" (Set (Var "z"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "y")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "y")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: ARYTM_1:28 (Bool  "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "st" (Bool (Bool (Set (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  )) & (Bool (Set (Var "z"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k11_arytm_3 :::"{}"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "z")) ")" )  ($#k2_arytm_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k11_arytm_3 :::"{}"::: ) ) "," (Set  "(" (Set (Var "x"))  ($#k8_arytm_2 :::"*'"::: )  (Set  "(" (Set (Var "y"))  ($#k1_arytm_1 :::"-'"::: )  (Set (Var "z")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))) ;